aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ide_slave.ml
diff options
context:
space:
mode:
authorletouzey2011-05-18 13:31:29 +0000
committerletouzey2011-05-18 13:31:29 +0000
commitd85e6bd09c32291e20962e29d739f2ffbe23c98f (patch)
tree607c08c811b245f8a8f06f43d28b66dfa2abdd2b /toplevel/ide_slave.ml
parent7e52f7728dcfcede7e40455385f3eef05a499c0d (diff)
Coqide: allow the use of Abort (grant wish #2357)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14136 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/ide_slave.ml')
-rw-r--r--toplevel/ide_slave.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 72ebecfa70..ee231b0445 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -148,7 +148,7 @@ let rec attribute_of_vernac_command = function
(* Proof management *)
| VernacGoal _ -> [GoalStartingCommand]
- | VernacAbort _ -> [NavigationCommand]
+ | VernacAbort _ -> []
| VernacAbortAll -> [NavigationCommand]
| VernacRestart -> [NavigationCommand]
| VernacSuspend -> [NavigationCommand]