aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authoraspiwack2007-12-06 14:24:53 +0000
committeraspiwack2007-12-06 14:24:53 +0000
commit3e3fa18a066feae44c10fc6e072059f4e9914656 (patch)
tree6ff163fd7561bf8c0823c7508acf83b350d4511d /ide
parentfb75bd254df2eadfc8abd45a646dfe9b1c4a53b6 (diff)
Commit intermédiaire express de réparation de coqide.ml, que j'avais
tout cassé hier sans m'en rendre compte (le soucis de travailler sur un ordinateur où j'ai pas installé lablgtk2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index cda306eb29..9860870ca0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -13,9 +13,6 @@ open Vernacexpr
open Coq
open Ideutils
-let Option.get s = match s with
- | None -> failwith "Internal error in Option.get" | Some f -> f
-
let cb_ = ref None
let cb () = ((Option.get !cb_):GData.clipboard)
let last_cb_content = ref ""