remove needless file for us
authorblanchet
Wed, 15 Sep 2010 16:19:49 +0200
changeset 39416 868f22264662
parent 39415 8ebe8dbe16ba
child 39417 0be01cad5df4
remove needless file for us
src/Tools/Metis/FILES
--- a/src/Tools/Metis/FILES	Wed Sep 15 16:17:05 2010 +0200
+++ b/src/Tools/Metis/FILES	Wed Sep 15 16:19:49 2010 +0200
@@ -12,7 +12,6 @@
 Heap.sig Heap.sml
 Print.sig Print.sml
 Parse.sig Parse.sml
-Options.sig Options.sml
 Name.sig Name.sml
 NameArity.sig NameArity.sml
 Term.sig Term.sml