equal
deleted
inserted
replaced
19 # -clean delete databases/images after use (leaving Pure) |
19 # -clean delete databases/images after use (leaving Pure) |
20 # -notest make databases/images w/o running the examples |
20 # -notest make databases/images w/o running the examples |
21 # -noexec don't execute, just check settings and IsaMakefiles |
21 # -noexec don't execute, just check settings and IsaMakefiles |
22 |
22 |
23 |
23 |
|
24 . $ISABELLE_HOME/lib/scripts/getplatform |
|
25 export ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM" |
|
26 |
24 set -e #fail immediately upon errors |
27 set -e #fail immediately upon errors |
25 |
28 |
26 # process command line switches |
29 # process command line switches |
27 CLEAN="off"; |
30 CLEAN="off"; |
28 FORCE="on"; |
31 FORCE="on"; |
40 *) echo "Bad flag for makeall: $A" |
43 *) echo "Bad flag for makeall: $A" |
41 echo "Usage: makeall [-noforce] [-clean] [-notest] [-noexec]" |
44 echo "Usage: makeall [-noforce] [-clean] [-notest] [-noexec]" |
42 exit ;; |
45 exit ;; |
43 esac |
46 esac |
44 done |
47 done |
45 |
|
46 |
|
47 . $ISABELLE_HOME/lib/scripts/getplatform |
|
48 export ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM" |
|
49 |
48 |
50 |
49 |
51 echo Started at `date` |
50 echo Started at `date` |
52 echo Source=`pwd` |
51 echo Source=`pwd` |
53 echo Destination=$ISABELLE_OUTPUT_DIR |
52 echo Destination=$ISABELLE_OUTPUT_DIR |