From a7a1ec22bc2aa06cc419f7012863656c3aec5871 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 9 Jun 2015 10:49:02 +0200
Subject: STM: silly mistake in jumping back to an old state (Close #4249)

---
 test-suite/ide/bug4249.fake | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test-suite/ide/bug4249.fake

(limited to 'test-suite/ide')

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