blob: 13e264c09c4426ab40ac392c5e0499152fced2a3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
# 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
rm -f misc/deps/théorèmes/*.v
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
exit 0
else
exit 1
fi
fi
|
