]> matita.cs.unibo.it Git - helm.git/commitdiff
mywget renamed in helm_wget; autoconf used for helm_wget
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Dec 2000 17:52:54 +0000 (17:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Dec 2000 17:52:54 +0000 (17:52 +0000)
helm/interface/.cvsignore
helm/interface/Makefile.in
helm/interface/configure.in
helm/interface/getter.ml
helm/interface/helm_wget.in [new file with mode: 0755]
helm/interface/mywget [deleted file]

index d93fd19b18f8a8ec8cec0caf22e45878bba2807e..b01badb8efc08293380e98d65d031f29298d56a3 100644 (file)
@@ -16,6 +16,7 @@ output2.ps
 
 Makefile
 configuration.ml
+helm_wget
 configure
 config.log
 config.cache
index 39328094c8ae0db36e4f5c75c247b9b922eb39b6..b31b68e616f3a7bc37069cd4de48edc5564703ba 100644 (file)
@@ -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
 
index 71fdf4a9381e308693834c841ab624c5bcdad810..b73c9b2b441bbf931705ae8e4d5dd8bcfc7a68fb 100644 (file)
@@ -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])
index d3da5a579da24f566d5f26eace108518226cfd61..a72db448bf7b70df3971b27e37a48dfa9e79c95d 100644 (file)
@@ -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 (executable)
index 0000000..b0d29df
--- /dev/null
@@ -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 (executable)
index c6f3205..0000000
+++ /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";
-}