From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Dec 2000 17:52:54 +0000 (+0000)
Subject: mywget renamed in helm_wget; autoconf used for helm_wget
X-Git-Tag: nogzip~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=274cfc6d7faa3c8bbeaac47fc48365128f01c5bb;p=helm.git

mywget renamed in helm_wget; autoconf used for helm_wget
---

diff --git a/helm/interface/.cvsignore b/helm/interface/.cvsignore
index d93fd19b1..b01badb8e 100644
--- a/helm/interface/.cvsignore
+++ b/helm/interface/.cvsignore
@@ -16,6 +16,7 @@ output2.ps
 
 Makefile
 configuration.ml
+helm_wget
 configure
 config.log
 config.cache
diff --git a/helm/interface/Makefile.in b/helm/interface/Makefile.in
index 39328094c..b31b68e61 100644
--- a/helm/interface/Makefile.in
+++ b/helm/interface/Makefile.in
@@ -175,11 +175,11 @@ clean:
            mmlinterface.opt mmlinterface2 mmlinterface2.opt
 
 install:
-	cp mmlinterface mmlinterface.opt $(HELM_BIN_DIR)
+	cp mmlinterface mmlinterface.opt helm_wget $(HELM_BIN_DIR)
 
 distclean:
-	rm -f Makefile configuration.ml configure config.log config.cache \
-         config.status
+	rm -f Makefile configuration.ml helm_wget configure config.log \
+         config.cache config.status
 
 .PHONY: install distclean clean
 
diff --git a/helm/interface/configure.in b/helm/interface/configure.in
index 71fdf4a93..b73c9b2b4 100644
--- a/helm/interface/configure.in
+++ b/helm/interface/configure.in
@@ -35,8 +35,14 @@ if test "$RES" != "Asked" ; then
 fi
 AC_CACHE_SAVE
 
+AC_PATH_PROG(PERL_BINARY,perl,no)
+if test $PERL_BINARY = no ; then
+   AC_MSG_ERROR(Could not find perl)
+fi
+
 AC_SUBST(OCAML_ROOT)
 AC_SUBST(HELM_BIN_DIR)
 AC_SUBST(HELM_DEFAULT_CONFIGURATION_DIR)
+AC_SUBST(PERL_BINARY)
 
-AC_OUTPUT([Makefile configuration.ml])
+AC_OUTPUT([Makefile configuration.ml helm_wget])
diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml
index d3da5a579..a72db448b 100644
--- a/helm/interface/getter.ml
+++ b/helm/interface/getter.ml
@@ -20,7 +20,7 @@ module MapOfStrings = Map.Make(OrderedStrings);;
 
 let read_index url =
  let module C = Configuration in
-  if Sys.command ("./mywget " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^
+  if Sys.command ("helm_wget " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^
    C.indexname ^ "\"") <> 0
   then
    raise (ErrorGetting url) ;
@@ -108,7 +108,7 @@ let get_file uri =
     begin
      let url = url_of_uri uri in
       (*CSC: use -q for quiet mode *)
-      if Sys.command ("./mywget " ^ dir ^ " \"" ^ url ^"\"") <> 0
+      if Sys.command ("helm_wget " ^ dir ^ " \"" ^ url ^"\"") <> 0
       then
        raise (ErrorGetting url) ;
     end ;
diff --git a/helm/interface/helm_wget.in b/helm/interface/helm_wget.in
new file mode 100755
index 000000000..b0d29df47
--- /dev/null
+++ b/helm/interface/helm_wget.in
@@ -0,0 +1,19 @@
+#!@PERL_BINARY@
+
+if ($#ARGV != 1) {
+ print STDERR "Usage: mywget prefix URL\n";
+ exit -1;
+}
+
+my ($prefix,$URL) = @ARGV;
+if ($URL =~ /^file:\//) {
+ $URL =~ s/^file:\///;
+ my $command = "mkdir -p $prefix ; cp $URL $prefix";
+ print "$command\n";
+ system($command) == 0
+  or die "\"$command\" error";
+} else {
+ my $command = "wget -c -P $prefix $URL";
+ system($command) == 0
+  or die "\"$command\" error";
+}
diff --git a/helm/interface/mywget b/helm/interface/mywget
deleted file mode 100755
index c6f3205b7..000000000
--- a/helm/interface/mywget
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/usr/bin/perl
-
-if ($#ARGV != 1) {
- print STDERR "Usage: mywget prefix URL\n";
- exit -1;
-}
-
-my ($prefix,$URL) = @ARGV;
-if ($URL =~ /^file:\//) {
- $URL =~ s/^file:\///;
- my $command = "mkdir -p $prefix ; cp $URL $prefix";
- print "$command\n";
- system($command) == 0
-  or die "\"$command\" error";
-} else {
- my $command = "wget -c -P $prefix $URL";
- system($command) == 0
-  or die "\"$command\" error";
-}