From af29dd0dc131674d1cb0007d86b2c12500556aad Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 6 Sep 2011 13:27:34 +0000
Subject: ide/preferences.ml: apparently no `META in Gdk.Tags.modifier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14458 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/preferences.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 45d2d88779..8d7723bb07 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -23,7 +23,6 @@ let mod_to_str (m:Gdk.Tags.modifier) =
     | `MOD5 -> "<Mod5>"
     | `CONTROL -> "<Control>"
     | `SHIFT -> "<Shift>"
-    | `META -> "<Meta>"
     |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
 
 let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
-- 
cgit v1.2.3