# HG changeset patch
# User wenzelm
# Date 860772615 -7200
# Node ID bd33e7aae062fc457cce9adc098971a34d93bcfb
# Parent  998cb95fdd43d10103ce80ee0ceffaa4e57c6b70
fixed { ... } shell syntax to accomodate bash 2.x;

diff -r 998cb95fdd43 -r bd33e7aae062 bin/isabelle
--- 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
diff -r 998cb95fdd43 -r bd33e7aae062 bin/isatool
--- 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
diff -r 998cb95fdd43 -r bd33e7aae062 build
--- 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
diff -r 998cb95fdd43 -r bd33e7aae062 lib/Tools/doc
--- 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
diff -r 998cb95fdd43 -r bd33e7aae062 lib/Tools/findlogics
--- 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)
diff -r 998cb95fdd43 -r bd33e7aae062 lib/scripts/run-polyml
--- 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"
diff -r 998cb95fdd43 -r bd33e7aae062 lib/scripts/run-smlnj
--- 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();"
diff -r 998cb95fdd43 -r bd33e7aae062 lib/scripts/run-smlnj-0.93
--- 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