# HG changeset patch
# User wenzelm
# Date 1182426803 -7200
# Node ID 51c23b0929fba23c18799f98326034caf3c0821e
# Parent  f274975039b21f2cb64dbaadf271d9dddd3daa23
added Id;

diff -r f274975039b2 -r 51c23b0929fb src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Thu Jun 21 13:49:27 2007 +0200
+++ b/src/Tools/Metis/metis.ML	Thu Jun 21 13:53:23 2007 +0200
@@ -1,3 +1,4 @@
+(* $Id$ *)
 (******************************************************************)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)