diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-12 11:51:21 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-12 11:51:21 +0100 |
| commit | a622c4c951f559fa05d45a45b4b25ace00793281 (patch) | |
| tree | 6374524264f598772affbf2f22ac5feed4b2c8a8 /ide/session.mli | |
| parent | 1142dab2ee08b23cdf97cdf52d5dc7ecd7768967 (diff) | |
CoqIDE: Errors page gets red if not empty
Diffstat (limited to 'ide/session.mli')
| -rw-r--r-- | ide/session.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/session.mli b/ide/session.mli index 3ed1b1ee3..527e1d170 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -13,6 +13,7 @@ class type ['a] page = object inherit GObj.widget method update : 'a -> unit + method on_update : callback:('a -> unit) -> unit end type errpage = (int * string) list page |