aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isa/thy/test.ML
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-02-01 12:49:52 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-02-01 12:49:52 +0000
commit65fe1811e9c7832f4b483cd90f07fcf04747671d (patch)
treeded1cdd6ca9c79ad592424bb37890f0ad05c6407 /etc/isa/thy/test.ML
parent7a0f9b6506a1c903c2d512fd8cd2d0fd1594d3bf (diff)
Test case for file recognition bug.
Diffstat (limited to 'etc/isa/thy/test.ML')
-rw-r--r--etc/isa/thy/test.ML5
1 files changed, 5 insertions, 0 deletions
diff --git a/etc/isa/thy/test.ML b/etc/isa/thy/test.ML
new file mode 100644
index 00000000..6a434570
--- /dev/null
+++ b/etc/isa/thy/test.ML
@@ -0,0 +1,5 @@
+(* Test case for wrong file type
+ bug report by jv@ddre.dk
+
+ This file should be ML, not theory!
+*) \ No newline at end of file