# HG changeset patch
# User blanchet
# Date 1284560389 -7200
# Node ID 868f222646629642e139ffd08472af1c382502fe
# Parent  8ebe8dbe16ba9e094a365081a2b1962fc5f13be2
remove needless file for us

diff -r 8ebe8dbe16ba -r 868f22264662 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