Notes about strange filenames

2 files changed, 27 insertions, 0 deletions

diff --git a/etc/TESTS b/etc/TESTS
index c16db0e7..222e5958 100644
--- a/etc/TESTS
+++ b/etc/TESTS
@@ -5,6 +5,22 @@ See testing-log.txt for log of tests conducted.
 Please add to that file!
 
 
+22.3.00 FILENAME ESCAPES PROBLEM [All provers, probably]
+========================================================
+
+  Filename substitution %s in settings including proof-shell-cd-cmd,
+  proof-shell-inform-file-{retracted,processed}-cmd, may need
+  to add escape characters peculiar to the proof assistant syntax.
+
+  Test cases:
+
+     ln -s ProofGeneral \\backslash  
+     ln -s ProofGeneral \"quote
+
+  Then try scripting with example files for each prover,
+  i.e.  \"quote/coq/example.v, etc.
+
+
 1.2.99 FILE RECOGNITION PROBLEM  [Isabelle]
 ===========================================
 
diff --git a/etc/testing-log.txt b/etc/testing-log.txt
index 0e86e183..4447e73e 100644
--- a/etc/testing-log.txt
+++ b/etc/testing-log.txt
@@ -1,3 +1,14 @@
+Wed Mar 22 13:45:34 GMT 2000 da 
+
+ Tested file name quoting problem with Coq, Isabelle, LEGO.
+  
+   \ quoting triggers bug in Isabelle (complaint about pathname)
+   " quoting not allowed in LEGO, \ quoting not needed.
+   Coq works well with either.
+	
+
+--------
+	
 Wed Nov 17 13:43:11 GMT 1999
 
  Tested compiled version.  Seems to work well for XEmacs!