aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2018-11-19 15:45:05 +0100
committerVincent Laporte2019-03-19 08:40:19 +0000
commitab276ee0e26c52e9ee049077e95e2454b17da203 (patch)
treed18b69b8c9334663a4c223968f66b4c657535de8
parent05e15386fad28f138e6e889c421242c60b9cb39a (diff)
CoqIDE: wm_name and wm_class are now packed into wmclass.
-rw-r--r--ide/coqide.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0acbef1ad7..4b08a8795c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -359,7 +359,7 @@ let print sn =
Filename.quote (Filename.basename f_name) ^ " | " ^ cmd_print#get
in
let w = GWindow.window ~title:"Print" ~modal:true
- ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" ()
+ ~position:`CENTER ~wmclass:("CoqIDE","CoqIDE") ()
in
let v = GPack.vbox ~spacing:10 ~border_width:10 ~packing:w#add ()
in
@@ -939,7 +939,7 @@ let emit_to_focus window sgn =
let build_ui () =
let w = GWindow.window
- ~wm_class:"CoqIde" ~wm_name:"CoqIde"
+ ~wmclass:("CoqIde","CoqIde")
~width:window_width#get ~height:window_height#get
~title:"CoqIde" ()
in