removed obsolete ML_SUFFIX;
authorwenzelm
Sat, 14 Jun 2008 17:26:09 +0200
changeset 27201 e0323036bcf2
parent 27200 00b7b55b61bd
child 27202 1a604efd267d
removed obsolete ML_SUFFIX;
bin/isabelle-process
lib/Tools/findlogics
--- a/bin/isabelle-process	Sat Jun 14 17:26:07 2008 +0200
+++ b/bin/isabelle-process	Sat Jun 14 17:26:09 2008 +0200
@@ -164,7 +164,7 @@
     INFILE=""
     ;;
   */*)
-    INFILE="$INPUT$ML_SUFFIX"
+    INFILE="$INPUT"
     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
     ;;
   *)
@@ -177,7 +177,7 @@
     do
       DIR="$DIR/$ML_IDENTIFIER"
       ISA_PATH="$ISA_PATH  $DIR\n"
-      [ -z "$INFILE" -a -f "$DIR/$INPUT$ML_SUFFIX" ] && INFILE="$DIR/$INPUT$ML_SUFFIX"
+      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
     done
     IFS="$ORIG_IFS"
 
@@ -197,11 +197,11 @@
     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
     ;;
   */*)
-    OUTFILE="$OUTPUT$ML_SUFFIX"
+    OUTFILE="$OUTPUT"
     ;;
   *)
     mkdir -p "$ISABELLE_OUTPUT"
-    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT$ML_SUFFIX"
+    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
     ;;
 esac
 
--- a/lib/Tools/findlogics	Sat Jun 14 17:26:07 2008 +0200
+++ b/lib/Tools/findlogics	Sat Jun 14 17:26:09 2008 +0200
@@ -34,7 +34,7 @@
   for FILE in "$DIR"/*
   do
     if [ -f "$FILE" ]; then
-      NAME=$(basename "$FILE" "$ML_SUFFIX")
+      NAME=$(basename "$FILE")
       LOGICS="$LOGICS $NAME"
     fi
   done