diff options
| -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 |