diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 5 | ||||
| -rw-r--r-- | ide/tags.ml | 2 |
2 files changed, 1 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 4b08a8795c..386bd8047c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1303,11 +1303,6 @@ let build_ui () = let _ = source_style#connect#changed ~callback:refresh_style in let _ = source_language#connect#changed ~callback:refresh_language in - (* Color configuration *) - Tags.Script.incomplete#set_property - (`BACKGROUND_STIPPLE - (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); - (* Showtime ! *) w#show (); w 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 = |