aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-04-08 15:50:39 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-04-08 15:50:39 +0000
commit0cf541452e6bb56ddddfae6bd9c1e08fbd47a687 (patch)
treee78edf4a33bdc4836bf10f589c07965d22109941
parentaa40ae5b2fe08d65f62200e65fe6da9467f55e51 (diff)
Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branch
(r12063) for smooth compilation/installation under Solaris (/bin/sh -> /bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than in if). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile32
-rw-r--r--Makefile.build6
-rw-r--r--Makefile.stage11
-rwxr-xr-xbuild2
-rwxr-xr-xconfigure4
-rwxr-xr-xinstall.sh2
6 files changed, 24 insertions, 23 deletions
diff --git a/Makefile b/Makefile
index 7eb478522..609e4b76e 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
#######################################################################
# v # The Coq Proof Assistant / The Coq Development Team #
-# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay #
+# <O___,, # INRIA-Rocquencourt & LRI-CNRS-osay #
# \VV/ #############################################################
# // # This file is distributed under the terms of the #
# # GNU Lesser General Public License Version 2.1 #
@@ -66,21 +66,21 @@
# but doesn't care if this build fails. This can be quite surprising,
# see in particular the -include in Makefile.stage*
-
+export SHELL:=/bin/bash
# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !!
export FIND_VCS_CLAUSE:='(' \
- -name '{arch}' -or \
- -name '.svn' -or \
- -name '_darcs' -or \
- -name '.git' -or \
- -name '.bzr' -or \
- -name 'debian' -or \
- -name "$${GIT_DIR}" -or \
+ -name '{arch}' -o \
+ -name '.svn' -o \
+ -name '_darcs' -o \
+ -name '.git' -o \
+ -name '.bzr' -o \
+ -name 'debian' -o \
+ -name "$${GIT_DIR}" -o \
-name '_build' \
-')' -prune -or
-export PRUNE_CHECKER := -wholename ./checker/\* -prune -or
+')' -prune -o
+export PRUNE_CHECKER := -wholename ./checker/\* -prune -o
FIND_PRINTF_P:=-print | sed 's|^\./||'
@@ -189,16 +189,16 @@ clean: objclean cruftclean depclean docclean devdocclean
objclean: archclean indepclean
cruftclean: ml4clean
- find . -name '*~' -or -name '*.annot' | xargs rm -f
+ find . -name '*~' -o -name '*.annot' | xargs rm -f
rm -f gmon.out core
indepclean:
rm -f $(GENFILES)
rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
- find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f
+ find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
find . -name '*_mod.ml' | xargs rm -f
- find plugins test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
+ find plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
rm -f */*.pp[iox] plugins/*/*.pp[iox]
rm -rf $(SOURCEDOCDIR)
rm -f toplevel/mltop.byteml toplevel/mltop.optml
@@ -227,7 +227,7 @@ archclean: clean-ide cleantheories
rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT)
rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE)
- find . -name '*.cmx' -or -name '*.cmxs' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f
+ find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
rm -f $(TOOLS) $(CSDPCERT)
rm -rf _build myocamlbuild_config.ml
@@ -254,7 +254,7 @@ distclean: clean cleanconfig
cleantheories:
rm -f states/*.coq
- find theories -name '*.vo' -or -name '*.glob' | xargs rm -f
+ find theories -name '*.vo' -o -name '*.glob' | xargs rm -f
devdocclean:
find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \;
diff --git a/Makefile.build b/Makefile.build
index e7e409833..b3b3b269b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -365,12 +365,12 @@ else
# coq-interface and coq-parser are direct calls to coqtop with some dynlink
bin/coq-interface$(EXE):
- echo "#!/bin/sh" > $@
+ echo "#!/bin/bash" > $@
echo 'exec '$(BINDIR)'/coqtop -require CoqInterface' >> $@
chmod +x $@
bin/coq-parser$(EXE):
- echo "#!/bin/sh" > $@
+ echo "#!/bin/bash" > $@
echo 'exec '$(BINDIR)'/coqtop -batch -l CoqParser' >> $@
chmod +x $@
@@ -889,7 +889,7 @@ else
endif
%.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
$(SHOW)'CAMLP4DEPS $<'
- $(HIDE)( /bin/echo -n '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
+ $(HIDE)( printf "%s" '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
|| ( RV=$$?; rm -f "$@"; exit $${RV} )
%.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML) %.ml4.d
diff --git a/Makefile.stage1 b/Makefile.stage1
index a60d388fc..c39a6372e 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -6,6 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
+export SHELL:=/bin/bash
include Makefile.build
# All includes must be declared secondary, otherwise make will delete
diff --git a/build b/build
index 26237b705..6edc6b0f4 100755
--- a/build
+++ b/build
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
FLAGS=
OCAMLBUILD=ocamlbuild
diff --git a/configure b/configure
index 88bb0fe52..7476485fd 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
##################################
#
@@ -293,7 +293,7 @@ case $arch_spec in
ARCH=`/usr/bin/uname -s`
else
echo "I can not automatically find the name of your architecture"
- echo -n\
+ printf "%s"\
"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
read ARCH
fi
diff --git a/install.sh b/install.sh
index 277222f58..c2f8215b0 100755
--- a/install.sh
+++ b/install.sh
@@ -1,4 +1,4 @@
-#! /bin/sh
+#! /bin/bash
dest="$1"
shift