/usr/bin/update-gap-workspace is in gap-core 4r8p6-2.
This file is owned by root:root, with mode 0o755.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 | #! /bin/sh
set -e
GAP="/usr/bin/gap"
if ! test -x "$GAP"; then
exit 0;
fi
if test `id -u` = 0; then
WORKSPACE=/var/lib/gap/workspace
else
WORKSPACE=$HOME/gap/workspace
fi
case $1 in
delete) echo -n "Deleting GAP workspace $WORKSPACE.gz: "
rm -f $WORKSPACE.gz
echo "done.";;
''|update) echo -n "Updating GAP workspace $WORKSPACE.gz: "
rm -f $WORKSPACE.gz
mkdir -p `dirname $WORKSPACE`
echo 'SaveWorkspace("'$WORKSPACE'");' | $GAP -q -r -R >/dev/null
gzip --best $WORKSPACE
echo "done.";;
*)
echo "$0 update"
echo " Update GAP workspace in $WORKSPACE.gz"
echo
echo "$0 delete"
echo " Delete GAP workspace in $WORKSPACE.gz"
;;
esac;
|