summaryrefslogtreecommitdiff
path: root/test-suite/misc/deps-utf8.sh
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/misc/deps-utf8.sh')
-rwxr-xr-xtest-suite/misc/deps-utf8.sh9
1 files changed, 5 insertions, 4 deletions
diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh
index 13e264c0..acb45b22 100755
--- a/test-suite/misc/deps-utf8.sh
+++ b/test-suite/misc/deps-utf8.sh
@@ -1,15 +1,16 @@
+#!/bin/sh
# Check reading directories matching non pure ascii idents
# See bug #5715 (utf-8 working on macos X and linux)
# Windows is still not compliant
-a=`uname`
-if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then
+a=$(uname)
+if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then
rm -f misc/deps/théorèmes/*.v
-tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX)
$coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v
R=$?
$coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v
S=$?
-if [ $R = 0 -a $S = 0 ]; then
+if [ $R = 0 ] && [ $S = 0 ]; then
exit 0
else
exit 1