diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-22 12:55:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-22 12:55:13 +0000 |
| commit | 04dae31678bbb6eb58e957a88625de44da1fa97c (patch) | |
| tree | 64d52161659c25478e0480c652028ae289b65a31 | |
| parent | aaf47bf358301b0f09e3500ea9eb3f596b7ee7c5 (diff) | |
Added test files to check stupid filename for directories.
| -rw-r--r-- | etc/isa/\backslashname/test.ML | 3 | ||||
| -rw-r--r-- | etc/isa/\backslashname/test.thy | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/etc/isa/\backslashname/test.ML b/etc/isa/\backslashname/test.ML new file mode 100644 index 00000000..c5f31182 --- /dev/null +++ b/etc/isa/\backslashname/test.ML @@ -0,0 +1,3 @@ +(* Scripting here tests quotation mechanism for filenames. *) + +val a = 1; diff --git a/etc/isa/\backslashname/test.thy b/etc/isa/\backslashname/test.thy new file mode 100644 index 00000000..2ca5331f --- /dev/null +++ b/etc/isa/\backslashname/test.thy @@ -0,0 +1 @@ +test = Pure |