diff options
| author | Hugo Herbelin | 2018-11-19 15:45:46 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:19 +0000 |
| commit | 390e8b97482a3100e8d37e2e62a345f9267960e2 (patch) | |
| tree | 0d7a0f2c21b383529c91146f7a97f45ead09912d /ide/tags.ml | |
| parent | ab276ee0e26c52e9ee049077e95e2454b17da203 (diff) | |
CoqIDE: Stippling using bitmap no more supported for incomplete Qed.
Was formerly displaying a stippled ("pointillé") light blue. Now only
a light blue.
Diffstat (limited to 'ide/tags.ml')
| -rw-r--r-- | ide/tags.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/tags.ml b/ide/tags.ml index 60195e8acb..e919a64278 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -24,7 +24,7 @@ struct let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] - let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true] + let incomplete = make_tag table ~name:"incomplete" [] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) let ephemere = |