New file mentioning some test cases.

1 files changed, 32 insertions, 0 deletions

diff --git a/etc/TESTS b/etc/TESTS
new file mode 100644
index 00000000..a5936b05
--- /dev/null
+++ b/etc/TESTS
@@ -0,0 +1,32 @@
+Some test cases for Proof General.
+==================================
+
+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).
+
+  
+
+    
+  
+