# HG changeset patch
# User wenzelm
# Date 1213457169 -7200
# Node ID e0323036bcf2d4b6cf903f2bf796784cd89b17dd
# Parent  00b7b55b61bd7d500cccc5bca24143af2194f345
removed obsolete ML_SUFFIX;

diff -r 00b7b55b61bd -r e0323036bcf2 bin/isabelle-process
--- 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
 
diff -r 00b7b55b61bd -r e0323036bcf2 lib/Tools/findlogics
--- 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