]> matita.cs.unibo.it Git - helm.git/commitdiff
no longer uses Shell library
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 6 Jul 2005 15:49:45 +0000 (15:49 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 6 Jul 2005 15:49:45 +0000 (15:49 +0000)
helm/ocaml/getter/http_getter_env.ml

index 74e32c22f265ceabd16d0b2affb8a08148da573b..c12709dcc562c652d41e09baac1547f44b033072 100644 (file)
@@ -62,11 +62,7 @@ let prefixes = lazy (
         acc)
     [] prefixes)
 
-let host =
-  lazy
-    (let buf = Buffer.create 20 in
-    Shell.call ~stdout:(Shell.to_buffer buf) [Shell.cmd "hostname" ["-f"]];
-    Pcre.replace ~pat:"\n+$" (Buffer.contents buf))
+let host = lazy (Http_getter_misc.backtick "hostname -f")
 
 let my_own_url =
   lazy