Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed { ... } shell syntax to accomodate bash 2.x;
authorwenzelm
Fri, 11 Apr 1997 17:30:15 +0200
changeset 2936 bd33e7aae062
parent 2935 998cb95fdd43
child 2937 9d31c472d0b0
fixed { ... } shell syntax to accomodate bash 2.x;
bin/isabelle file | annotate | diff | comparison | revisions
bin/isatool file | annotate | diff | comparison | revisions
build file | annotate | diff | comparison | revisions
lib/Tools/doc file | annotate | diff | comparison | revisions
lib/Tools/findlogics file | annotate | diff | comparison | revisions
lib/scripts/run-polyml file | annotate | diff | comparison | revisions
lib/scripts/run-smlnj file | annotate | diff | comparison | revisions
lib/scripts/run-smlnj-0.93 file | annotate | diff | comparison | revisions 
--- a/bin/isabelle	Fri Apr 11 15:21:36 1997 +0200
+++ b/bin/isabelle	Fri Apr 11 17:30:15 1997 +0200
@@ -11,7 +11,7 @@
 
 ISABELLE_HOME=$(dirname $0)/..
 . $ISABELLE_HOME/lib/scripts/getsettings || \
-  { echo "$PRG probably not called from its original place!"; exit 2 }
+  { echo "$PRG probably not called from its original place!"; exit 2; }
 
 
 ## diagnostics
@@ -104,7 +104,7 @@
   shift
 fi
 
-[ $# -ne 0 ] && { echo "Bad args: $*"; usage }
+[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
 
 
 ## check ML system
--- a/bin/isatool	Fri Apr 11 15:21:36 1997 +0200
+++ b/bin/isatool	Fri Apr 11 17:30:15 1997 +0200
@@ -12,7 +12,7 @@
 
 ISABELLE_HOME=$(dirname $0)/..
 . $ISABELLE_HOME/lib/scripts/getsettings || \
-  { echo "$PRG probably not called from its original place!"; exit 2 }
+  { echo "$PRG probably not called from its original place!"; exit 2; }
 
 
 ## diagnostics
--- a/build	Fri Apr 11 15:21:36 1997 +0200
+++ b/build	Fri Apr 11 17:30:15 1997 +0200
@@ -11,7 +11,7 @@
 
 ISABELLE_HOME=$(dirname $0)
 . $ISABELLE_HOME/lib/scripts/getsettings || \
-  { echo "$PRG probably not called from its original place!"; exit 2 }
+  { echo "$PRG probably not called from its original place!"; exit 2; }
 
 
 ## diagnostics
--- a/lib/Tools/doc	Fri Apr 11 15:21:36 1997 +0200
+++ b/lib/Tools/doc	Fri Apr 11 17:30:15 1997 +0200
@@ -30,7 +30,7 @@
 ## args
 
 DOC=""
-[ $# -ge 1 ] && { DOC="$1"; shift }
+[ $# -ge 1 ] && { DOC="$1"; shift; }
 
 [ $# -ne 0 -o "$DOC" = "-?" ] && usage
 
@@ -45,7 +45,7 @@
 else
   for DIR in $ISABELLE_DOCS
   do
-    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi }
+    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
   done
   fail "Unknown Isabelle document: $DOC"  
 fi
--- a/lib/Tools/findlogics	Fri Apr 11 15:21:36 1997 +0200
+++ b/lib/Tools/findlogics	Fri Apr 11 17:30:15 1997 +0200
@@ -36,4 +36,4 @@
   done
 done
 
-echo $({ for L in $LOGICS; do echo $L; done } | sort | uniq)
+echo $({ for L in $LOGICS; do echo $L; done; } | sort | uniq)
--- a/lib/scripts/run-polyml	Fri Apr 11 15:21:36 1997 +0200
+++ b/lib/scripts/run-polyml	Fri Apr 11 17:30:15 1997 +0200
@@ -44,12 +44,12 @@
 elif [ "$INFILE" -ef "$OUTFILE" ]; then
   DB="$INFILE"
 elif [ -n "$COPYDB" ]; then
-  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
+  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
   cp "$INFILE" "$OUTFILE" || fail_out
   chmod +w "$OUTFILE" || fail_out
   DB="$OUTFILE"
 else
-  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
+  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
   echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
   [ -f "$OUTFILE" ] || fail_out
   DB="$OUTFILE"
--- a/lib/scripts/run-smlnj	Fri Apr 11 15:21:36 1997 +0200
+++ b/lib/scripts/run-smlnj	Fri Apr 11 17:30:15 1997 +0200
@@ -39,11 +39,11 @@
 if [ -z "$OUTFILE" ]; then
   COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
 elif [ -n "$INFILE" -a ! "$INFILE" -ef "$OUTFILE" ]; then
-  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
+  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
   cp "$INFILE" "$OUTFILE" || fail_out
 fi
 
-[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
+[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
 
 MLTEXT="$EXIT $COMMIT $MLTEXT"
 MLEXIT="commit();"
--- a/lib/scripts/run-smlnj-0.93	Fri Apr 11 15:21:36 1997 +0200
+++ b/lib/scripts/run-smlnj-0.93	Fri Apr 11 17:30:15 1997 +0200
@@ -37,7 +37,7 @@
     mkdir -p "$OUTDIR" || fail_out
     MOVE=true
   fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
 fi
isabelle