Makefile
configuration.ml
+helm_wget
configure
config.log
config.cache
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
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])
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) ;
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 ;
--- /dev/null
+#!@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";
+}
+++ /dev/null
-#!/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";
-}