aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils/okey.ml
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-04 21:39:18 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-04 21:39:18 +0000
commitf0b936e7cb90000f5db6272b926cb13dc1a5c055 (patch)
tree63a5fefc70912f436c08b75f2e5813e62f407a93 /ide/utils/okey.ml
parent0187193260a57e6bac8fcde8eb0e66ccf3f37b9b (diff)
Fix coqide compilation with lablgtk 2.16
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15772 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/utils/okey.ml')
-rw-r--r--ide/utils/okey.ml10
1 files changed, 9 insertions, 1 deletions
diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml
index 6b174ecbe..580f1fbcb 100644
--- a/ide/utils/okey.ml
+++ b/ide/utils/okey.ml
@@ -47,6 +47,10 @@ let int_of_modifier = function
| `BUTTON3 -> 1024
| `BUTTON4 -> 2048
| `BUTTON5 -> 4096
+ | `HYPER -> 1 lsl 22
+ | `META -> 1 lsl 20
+ | `RELEASE -> 1 lsl 30
+ | `SUPER -> 1 lsl 21
let print_modifier l =
List.iter
@@ -65,7 +69,11 @@ let print_modifier l =
| `BUTTON2 -> "B2"
| `BUTTON3 -> "B3"
| `BUTTON4 -> "B4"
- | `BUTTON5 -> "B5")
+ | `BUTTON5 -> "B5"
+ | `HYPER -> "HYPER"
+ | `META -> "META"
+ | `RELEASE -> ""
+ | `SUPER -> "SUPER")
m)^" ")
)
l;