aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/demoisa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-16 15:42:14 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-16 15:42:14 +0000
commit3a44fd81f0e59c178ba3076a7e598a4d746908d1 (patch)
tree577f5135e853d313b74c724515639d4b5b48f76b /etc/demoisa
parent5a5c39dedd0f3491245d4cc1d156682e5b1fac91 (diff)
Test files for automatic multiple files.
Diffstat (limited to 'etc/demoisa')
-rw-r--r--etc/demoisa/A.ML1
-rw-r--r--etc/demoisa/B.ML1
-rw-r--r--etc/demoisa/C.ML1
-rw-r--r--etc/demoisa/D.ML1
-rw-r--r--etc/demoisa/README11
5 files changed, 15 insertions, 0 deletions
diff --git a/etc/demoisa/A.ML b/etc/demoisa/A.ML
new file mode 100644
index 00000000..69126156
--- /dev/null
+++ b/etc/demoisa/A.ML
@@ -0,0 +1 @@
+1; \ No newline at end of file
diff --git a/etc/demoisa/B.ML b/etc/demoisa/B.ML
new file mode 100644
index 00000000..85fa53ce
--- /dev/null
+++ b/etc/demoisa/B.ML
@@ -0,0 +1 @@
+2; \ No newline at end of file
diff --git a/etc/demoisa/C.ML b/etc/demoisa/C.ML
new file mode 100644
index 00000000..33fefea4
--- /dev/null
+++ b/etc/demoisa/C.ML
@@ -0,0 +1 @@
+3; \ No newline at end of file
diff --git a/etc/demoisa/D.ML b/etc/demoisa/D.ML
new file mode 100644
index 00000000..06b33ae0
--- /dev/null
+++ b/etc/demoisa/D.ML
@@ -0,0 +1 @@
+4; \ No newline at end of file
diff --git a/etc/demoisa/README b/etc/demoisa/README
new file mode 100644
index 00000000..be06a076
--- /dev/null
+++ b/etc/demoisa/README
@@ -0,0 +1,11 @@
+This is a test for automatic multiple file handling.
+
+Assert each of A.ML, B.ML, C.ML, D.ML in turn.
+
+Then retract B.ML.
+
+D.ML and C.ML should be automatically retracted.
+
+Set proof-tidy-response=nil to track what happens.
+
+ - da.