UPDATE-GAP-WORKSPACE(1) | User Commands | UPDATE-GAP-WORKSPACE(1) |
update-gap-workspace - manage a GAP workspace.
update-gap-workspace
update-gap-workspace update
update-gap-workspace delete
At start up, GAP load all libraries and packages available on the system. 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.
/var/lib/gap/workspace.gz:
gap(1), The `SaveWorkspace' function in the GAP manual.
Bill Allombert <ballombe@debian.org>
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>.
July 2003 | Debian |