debian man page for update-gap-workspace

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 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>.

Debian								     July 2003						   UPDATE-GAP-WORKSPACE(1)