From 115860adb8e0054b005fe08efc45d999b2f0f3c1 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 28 Jan 2010 22:10:08 +0000
Subject: 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
---
 Makefile                    |  3 ++-
 build                       |  2 +-
 configure                   |  2 +-
 dev/v8-syntax/check-grammar | 18 +++++++++---------
 install.sh                  |  4 +---
 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
-
-
-- 
cgit v1.2.3