# HG changeset patch
# User blanchet
# Date 1284558583 -7200
# Node ID c70a6c169a161001cf61eee588e417f9d27164a5
# Parent  7e8f49d412d672e96ce59fce1a8bbcf79da25ccc
tuning

diff -r 7e8f49d412d6 -r c70a6c169a16 src/Tools/Metis/make_metis
--- a/src/Tools/Metis/make_metis	Wed Sep 15 15:49:21 2010 +0200
+++ b/src/Tools/Metis/make_metis	Wed Sep 15 15:49:43 2010 +0200
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 #
-# make-metis - turn original Metis files into Isabelle ML source.
+# make_metis - turn original Metis files into Isabelle ML source.
 #
 # Structure declarations etc. are made local by wrapping into a
 # collective structure Metis.  Signature and functor definitions are
@@ -11,7 +11,7 @@
 (
   cat <<EOF
 (*
-   This file was generated by the "make-metis" script. The BSD License is used
+   This file was generated by the "make_metis" script. The BSD License is used
    with Joe Hurd's kind permission. Extract from a September 13, 2010 email
    written by Joe Hurd: