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/" | \