aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorppedrot2012-06-29 20:33:57 +0000
committerppedrot2012-06-29 20:33:57 +0000
commit4aef7ca15b99e9a3b0671ff11d61d6aaa31e16b6 (patch)
treedf4fbcad2fc88265e9fe2abda4e5f4d520f4377b
parentc77296fec78e5abf15d53f41b649d79204266581 (diff)
Reversed message display order in CoqIDE
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15504 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b1f7b96162..9c6baee693 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -731,7 +731,7 @@ object(self)
input_buffer#delete_mark sentence.stop;
done;
(* Return the list of info messages and the error *)
- (!info, !error)
+ (List.rev !info, !error)
method private show_error phrase loc msg = match loc with
| None ->