diff options
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index b223be3a4..9da46d2e6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1389,6 +1389,11 @@ let build_ui () = (* Color configuration *) Tags.set_processing_color (Tags.color_of_string prefs.processing_color); Tags.set_processed_color (Tags.color_of_string prefs.processed_color); + Tags.Script.incomplete#set_property + (`BACKGROUND_STIPPLE + (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); + Tags.Script.incomplete#set_property + (`BACKGROUND_GDK (Tags.get_processed_color ())); (* Showtime ! *) w#show () |