diff -r f5320aba6750 -r 3e41c9d29769 src/Tools/Metis/Makefile.FILES
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/Makefile.FILES	Wed Sep 15 22:20:10 2010 +0200
@@ -0,0 +1,10 @@
+include Makefile
+bin/mosml/Makefile.src:
+	mkdir -p `dirname $@`
+	echo > $@
+refresh_FILES:
+	echo $(POLYML_SRC) | \
+	sed "s/src\///g" | \
+	sed "s/ Tptp\.s[a-z][a-z]//g" | \
+	sed "s/ Options\.s[a-z][a-z]//g" \
+	> FILES