From fbfc1b8d6e9d95fcbacd3f4ab4921d6f3b01198e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 9 Jun 2015 13:30:35 +0200
Subject: STM: states coming from workers have no proof terminators (Close
 #4246)

Hence we reuse the ones in master.
---
 test-suite/ide/bug4246.fake | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/ide/bug4246.fake

(limited to 'test-suite')

diff --git a/test-suite/ide/bug4246.fake b/test-suite/ide/bug4246.fake
new file mode 100644
index 0000000000..16b552f679
--- /dev/null
+++ b/test-suite/ide/bug4246.fake
@@ -0,0 +1,14 @@
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { trivial. } # first error
+ADD { fail. }
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD { Qed. }
+WAIT
+EDIT_AT here
+ADD { Qed. }
+JOIN
-- 
cgit v1.2.3