From 04dae31678bbb6eb58e957a88625de44da1fa97c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 22 Mar 2000 12:55:13 +0000
Subject: Added test files to check stupid filename for directories.

---
 "etc/isa/\\backslashname/test.ML"  | 3 +++
 "etc/isa/\\backslashname/test.thy" | 1 +
 2 files changed, 4 insertions(+)
 create mode 100644 "etc/isa/\\backslashname/test.ML"
 create mode 100644 "etc/isa/\\backslashname/test.thy"

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
-- 
cgit v1.2.3