File: update-gap-workspace

package info (click to toggle)
gap 4r7p5-2
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 29,272 kB
  • ctags: 7,129
  • sloc: ansic: 107,802; xml: 46,868; sh: 3,548; perl: 2,329; makefile: 740; python: 94; asm: 62; awk: 6
file content (35 lines) | stat: -rw-r--r-- 680 bytes parent folder | download | duplicates (9)
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;