Fix holdep test case for functor keyword.

This dodges the Moscow ML compilation error caused by its attempt to compile functor.sml (now deleted) in its default mode.
HOL-Theorem-Prover · Jul 16, 2015 · 087daed · 087daed
1 parent 8c47c9d
commit 087daed
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/tools/Holmake/tests/brokenstrings/functor.sml b/tools/Holmake/tests/brokenstrings/functor.sml
diff --git a/tools/Holmake/tests/holdep/Holmakefile b/tools/Holmake/tests/holdep/Holmakefile
@@ -1,7 +1,7 @@
 INCLUDES = ../../../cmp
 
 .PHONY: test
-test:
+test: input expected_output
 	$(protect $(HOLDIR)/bin/holdeptool.exe) input > output
 	$(protect $(HOLDIR)/tools/cmp/cmp.exe) output expected_output
 

diff --git a/tools/Holmake/tests/holdep/expected_output b/tools/Holmake/tests/holdep/expected_output
@@ -8,6 +8,7 @@ baz
 data1
 data2
 foo
+functortest
 included1
 included2
 included3

diff --git a/tools/Holmake/tests/holdep/input b/tools/Holmake/tests/holdep/input
@@ -34,3 +34,6 @@ include included4
 datatype datafoo
 
 include included5 where type t = int
+
+open functortest
+functor funct(val x : int) =
diff --git a/tools/sequences/kernel b/tools/sequences/kernel
@@ -14,6 +14,7 @@ src/1
 !tools/Holmake/tests/depchain2/dir1
 !tools/Holmake/tests/altquote1
 !tools/Holmake/tests/brokenstrings
+!tools/Holmake/tests/holdep
 !src/1/theory_tests
 src/proofman
 [poly]bin/hol.bare