aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-18 15:02:52 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-18 15:02:52 +0000
commita5cf61907148d79e5627930ae78bfb0a393b617d (patch)
tree193537fe267675eca3042d22e996aedd8c8ecd1e /lib
parent655b95012717f3b9fba714f591dfdb39d0174200 (diff)
retablissement de Correctness (pas encore teste' cependant)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3016 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/system.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml
index f5af836cf..35584bf89 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -16,7 +16,6 @@ open Unix
let safe_getenv_def var def =
try
- print_string var;
Sys.getenv var
with Not_found ->
warning ("Environment variable "^var^" not found: using '"^def^"' .");