Deleted file

1 files changed, 0 insertions, 95 deletions

diff --git a/etc/TESTS b/etc/TESTS
deleted file mode 100644
index 222e5958..00000000
--- a/etc/TESTS
+++ /dev/null
@@ -1,95 +0,0 @@
-Some test cases for Proof General.
-==================================
-
-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]
-===========================================
-
-  Bug in regexp caused ML files to be recognized as
-  theory files when "thy" appeared in path.
-  Test case in etc/isa/thy/test.ML.
-
-
-15.1.99  LONG-LINE AND BACKSLASH PROBLEM ON SOLARIS
-===================================================
-
-  Test that etc/isa/long-line-backslash.ML can be processed
-  successfully.
-
-
-16.12.98 KILLING THE PROOF PROCESS
-==================================
-
-  Process some proof script buffer. Invoke 
-
-    M-x proof-shell-exit
-
-  Process should exit cleanly.
-  
-11.12.98  RUDELY KILLING THE ACTIVE SCRIPTING BUFFER
-====================================================
-
-  Start scripting with some buffer, after
-  having processed another buffer.
-
-  Kill it when scripting is only partly finished.
-
-  Scripting should be cleanly turned off and it
-  should be possible to resume retraction in the 
-  first buffer.
-
-  Moreover, this ensures that if the file is on the included
-  files list, yet has been only partly processed (e.g. because
-  Undo steps were taken), then it will be retracted and
-  removed from the included files list.
-
-  FIXME: Using C-x C-v to revert to saved version doesn't
-  seem to work because it renames the buffer or something.
-
-8.12.98  INHIBIT VARIABLES
-==========================
-
-  Test with proof-splash-inhibit=t
-
-  Test with proof-toolbar-inhibit=t
-  
-
-8.12.98  SCRIPTING FOR BUFFERS WITHOUT FILES.
-=============================================
-
-  Switch to a fresh buffer FOO which doesn't visit a file.
-  Do  M-x isa-mode RET.
-  Should succeed.
-  Try asserting commands, e.g. Goal "P-->P";
-
-  Switch to another fresh buffer BAR, turn on isa-mode.
-  Should succeed again.
-  Try asserting commands here, e.g. Goal "Q&Q --> Q";
-  Should give error "Cannot have more than one active scripting buffer".
-
-  Exit emacs.  Should query whether we want to save these
-  scripting buffers (maybe XEmacs only).
-
-
-    
-  
-