UPDATE-GAP-WORKSPACE(1) User Commands UPDATE-GAP-WORKSPACE(1)
NAME
update-gap-workspace - manage a GAP workspace.
SYNOPSIS
update-gap-workspace
update-gap-workspace update
Create or update the GAP workspace.
update-gap-workspace delete
Delete the GAP workspace.
DESCRIPTION
At start up, GAP load all libraries and packages available on the sys-
tem. This take several seconds. To save time, GAP can store the result
of this initialisation in a `workspace'. update-gap-workspace help to
manage such workspaces. update-gap-workspace can be run as root to
manage the system-wide workspace. update-gap-workspace can be run as a
normal user. In this case the workspace is stored in
$HOME/gap/workspace.gz.
Note that you need to rebuild the workspace each time GAP packages are
added, removed or updated. To automate that task, if the system-wide
workspace exists, it is automatically updated whenever a GAP-related
Debian package is installed or upgraded.
The gap script will automatically load such workspace at start up.
FILES
/var/lib/gap/workspace.gz:
The system-wide GAP workspace.
$HOME/gap/workspace.gz:
The user-specific GAP workspace.
SEE ALSO
gap(1), The `SaveWorkspace' function in the GAP manual.
AUTHOR
Bill Allombert <ballombe@debian.org>
NOTES
We are considering enabling the system-wide workspace per default,
though this feature could be too confusing for old-time GAP users. If
you have opinions about it, please mail <gap@packages.debian.org>.
Debian July 2003 UPDATE-GAP-WORKSPACE(1)
Generated by dwww version 1.15 on Sun Jun 16 16:40:02 CEST 2024.