aboutsummaryrefslogtreecommitdiff
path: root/etc
diff options
context:
space:
mode:
Diffstat (limited to 'etc')
-rw-r--r--etc/isa/\backslashname/test.ML8
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;