Rechercher une page de manuel
update-gap-workspace
Langue: en
Version: 312382 (ubuntu - 07/07/09)
Section: 1 (Commandes utilisateur)
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 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.
The gap script will automatically load such workspace at start up.
FILES
/var/lib/gap/workspace.gz:- The system-wide GAP workspace.
- 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 make the building of system-wide GAP workspace automatic when any GAP Debian packages are updated. The implementation is ready, but we are afraid this feature would be too confusing for old-time GAP users. If you have opinions about, please mail <gap@packages.debian.org>.Contenus ©2006-2024 Benjamin Poulain
Design ©2006-2024 Maxime Vantorre