UPDATE-GAP-WORKSPACE
Section: User Commands (1)
Updated: July 2003
Index
Return to Main Contents
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. 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>.
Index
- NAME
-
- SYNOPSIS
-
- DESCRIPTION
-
- FILES
-
- SEE ALSO
-
- AUTHOR
-
- NOTES
-
This document was created by
man2html,
using the manual pages.
Time: 17:03:00 GMT, April 27, 2024