]> matita.cs.unibo.it Git - helm.git/commitdiff
during update, asks the perl getter to update too
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Dec 2000 20:00:19 +0000 (20:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Dec 2000 20:00:19 +0000 (20:00 +0000)
helm/interface/getter.ml

index 39af104ccb3e38de26d64ec5e500d1e84cea7627..d79409c8933f8181e432f1b1d5b6ff73d84a2f71 100644 (file)
@@ -56,6 +56,8 @@ let rec mk_urls_of_uris =
          uris map
 ;;
 
+exception PerlGetterNotResponding;;
+
 let update () =
  let module C = Configuration in
   let fd = open_in C.servers_file in
@@ -72,7 +74,11 @@ let update () =
        Dbm.opendbm C.uris_dbm [Dbm.Dbm_wronly ; Dbm.Dbm_create] 0o660
       in
        MapOfStrings.iter (fun uri url -> Dbm.add dbm uri url) urls_of_uris ;
-       Dbm.close dbm
+       Dbm.close dbm ;
+       (* Inform also the Perl-getter *)
+       if Sys.command ("wget -O /dev/null http://localhost:8081/update") <> 0
+       then
+        raise PerlGetterNotResponding ;
 ;;
 
 (* url_of_uri : uri -> url *)