Comment about tripping bug in Isabelle

1 files changed, 8 insertions, 0 deletions

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;