--- a/src/Tools/Metis/make-metis Thu Jun 21 13:53:23 2007 +0200
+++ b/src/Tools/Metis/make-metis Thu Jun 21 13:53:53 2007 +0200
@@ -11,6 +11,8 @@
THIS=$(cd "$(dirname "$0")"; echo $PWD)
(
+ echo -n '(* $'
+ echo 'Id$ *)'
cat <<EOF
(******************************************************************)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
@@ -40,7 +42,7 @@
else
echo -e "$FILE (local)" >&2
echo "structure Metis = struct open Metis"
- cat < "metis-env.ML"
+ cat < "metis_env.ML"
"$THIS/scripts/mlpp" -c isabelle "src/$FILE"
echo "end;"
fi