diff options
Diffstat (limited to 'test-suite/misc/deps-utf8.sh')
| -rwxr-xr-x | test-suite/misc/deps-utf8.sh | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh new file mode 100755 index 00000000..13e264c0 --- /dev/null +++ b/test-suite/misc/deps-utf8.sh @@ -0,0 +1,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 |