diff options
| author | gareuselesinge | 2013-10-22 14:31:45 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-22 14:31:45 +0000 |
| commit | 8cb2656507f44b7342ac4b75f787dd8f832ada84 (patch) | |
| tree | 0221657d74a936199b9328a3f2af8e5ac0e17a6c | |
| parent | b16c1a41dc9e4a00abb734dc820fff396c338634 (diff) | |
STM: proper error message if the GUI edits_at a dummy state
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16909 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/stm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index f63cd9e4e5..85e9a30ab1 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1590,6 +1590,7 @@ type focus = { } let edit_at id = + if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else let vcs = VCS.backup () in let on_cur_branch id = let rec aux cur = |