summaryrefslogtreecommitdiff
path: root/ide/utils/configwin_messages.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:47:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:47:51 +0200
commitaa33547c764a229e22d323ca213d46ea221b903e (patch)
tree3894cb190f34bc1d2deee4322a674db641562ee0 /ide/utils/configwin_messages.ml
parent50dc9067e98ca001ad2e875011abab5da6fdb621 (diff)
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Remove non-DFSG contentsupstream/8.3.pl2+dfsg
Diffstat (limited to 'ide/utils/configwin_messages.ml')
-rw-r--r--ide/utils/configwin_messages.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml
index f8984462..26f5b61b 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/utils/configwin_messages.ml
@@ -30,9 +30,7 @@ let version = "1.2";;
let html_config = "Configwin bindings configurator for html parameters"
-let home =
- try Sys.getenv "HOME"
- with Not_found -> ""
+let home = System.home
let mCapture = "Capture";;
let mType_key = "Type key" ;;