574c352
#!/bin/sh
574c352
#
574c352
# Script borrowed from Debian.  Thanks to the Debian packagers.
574c352
574c352
set -e
574c352
574c352
GAP="/usr/bin/gap"
574c352
574c352
if ! test -x "$GAP"; then
574c352
    exit 0;
574c352
fi
574c352
574c352
if test `id -u` = 0; then
574c352
    WORKSPACE=/var/lib/gap/workspace
574c352
else
574c352
    WORKSPACE=$HOME/gap/workspace
574c352
fi
574c352
574c352
case $1 in
574c352
delete) echo -n "Deleting GAP workspace $WORKSPACE.gz: "
574c352
    rm -f $WORKSPACE.gz
574c352
    echo "done.";;
574c352
''|update) echo -n "Updating GAP workspace $WORKSPACE.gz: "
574c352
    rm -f $WORKSPACE.gz
574c352
    mkdir -p `dirname $WORKSPACE`
574c352
    echo 'SaveWorkspace("'$WORKSPACE'");' | $GAP -q -r -R >/dev/null
574c352
    gzip --best $WORKSPACE
574c352
    echo "done.";;
574c352
*)
574c352
    echo "$0 update"
574c352
    echo "  Update GAP workspace in $WORKSPACE.gz"
574c352
    echo
574c352
    echo "$0 delete"
574c352
    echo "  Delete GAP workspace in $WORKSPACE.gz"
574c352
    ;;
574c352
esac