src/Tools/Metis/make_metis
changeset 43268 c0eaa8b9bff5
parent 39448 64639ff50fcd
child 56281 03c3d1a7c3b8
--- a/src/Tools/Metis/make_metis	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/make_metis	Wed Jun 08 08:47:43 2011 +0200
@@ -40,7 +40,6 @@
     echo -e "$FILE" >&2
     "$THIS/scripts/mlpp" -c polyml "$FILE" | \
     perl -p -e \
-'s/type name$/type name = string/;'\
 's/\bref\b/Unsynchronized.ref/g;'\
 "`grep "^\(signature\|structure\|functor\)" $FILES | \
   sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \