From ba0ff9573efd0dadf2843605783b11714f91681d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 22 Mar 2000 13:10:00 +0000
Subject: Comment about tripping bug in Isabelle

---
 "etc/isa/\\backslashname/test.ML" | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git "a/etc/isa/\\backslashname/test.ML" "b/etc/isa/\\backslashname/test.ML"
index c5f31182..0691e38e 100644
--- "a/etc/isa/\\backslashname/test.ML"
+++ "b/etc/isa/\\backslashname/test.ML"
@@ -1,3 +1,11 @@
 (* Scripting here tests quotation mechanism for filenames. *)
 
+(* At the moment this trips a bug in Isabelle which objects
+   to filename of this directory.
+
+   Easy way to test for other provers is with a link,
+   \bizzare  \\<rightarrow> ProofGeneral/  then load \bizarre/coq/example.v, etc
+
+*)
+
 val a = 1;
-- 
cgit v1.2.3