Remove bashisms

As pointed out by Nima Hoda, bash is not installed everywhere... and
we really don't NEED bash anyway.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12701 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 14 insertions, 15 deletions

diff --git a/Makefile b/Makefile
index 14e582700..920bb2c00 100644
--- a/Makefile
+++ b/Makefile
@@ -215,7 +215,8 @@ docclean:
 	rm -f doc/*/*.ps doc/*/*.pdf 
 	rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html
 	rm -f doc/stdlib/html/*.html
-	rm -f doc/refman/euclid.ml{,i} doc/refman/heapsort.ml{,i}
+	rm -f doc/refman/euclid.ml doc/refman/euclid.mli
+	rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
 	rm -f doc/common/version.tex
 	rm -f doc/refman/*.eps doc/refman/Reference-Manual.html
 	rm -f doc/coq.tex
diff --git a/build b/build
index 6edc6b0f4..26237b705 100755
--- a/build
+++ b/build
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/sh
 
 FLAGS=
 OCAMLBUILD=ocamlbuild
diff --git a/configure b/configure
index c3aaa241a..75f3af155 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/sh
 
 ##################################
 #
diff --git a/dev/v8-syntax/check-grammar b/dev/v8-syntax/check-grammar
index 67da1bc51..194a55fe8 100755
--- a/dev/v8-syntax/check-grammar
+++ b/dev/v8-syntax/check-grammar
@@ -1,31 +1,31 @@
-#!/bin/bash
+#!/bin/sh
 # This scripts checks that the new grammar of Coq as defined in syntax-v8.tex
 # is consistent in the sense that all invoked non-terminals are defined
 
-defined-nt() {
+defined_nt() {
   grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\
     sort | sort -u
 }
 
-used-nt() {
+used_nt() {
   cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\
     sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u
 }
 
-used-term() {
+used_term() {
   cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\
     sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u
 }
 
-used-kwd() {
+used_kwd() {
   cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\
     sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u
 }
 
-defined-nt > def
-used-nt > use
-used-term > use-t
-used-kwd > use-k
+defined_nt > def
+used_nt > use
+used_term > use-t
+used_kwd > use-k
 diff def use > df
 
 ###############################
diff --git a/install.sh b/install.sh
index c2f8215b0..4b3abe5c6 100755
--- a/install.sh
+++ b/install.sh
@@ -1,4 +1,4 @@
-#! /bin/bash
+#! /bin/sh
 
 dest="$1"
 shift
@@ -9,5 +9,3 @@ for f; do
   install -d "$dest/$dn"
   install -m 644 $f "$dest/$dn/$bn"
 done
-
-