diff options
-rwxr-xr-x | test-suite/misc/deps-utf8.sh | 17 | ||||
-rw-r--r-- | test-suite/misc/deps/αβ/γδ.v | 4 | ||||
-rw-r--r-- | test-suite/misc/deps/αβ/εζ.v | 1 |
3 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh new file mode 100755 index 000000000..13e264c09 --- /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 diff --git a/test-suite/misc/deps/αβ/γδ.v b/test-suite/misc/deps/αβ/γδ.v new file mode 100644 index 000000000..f43a2d657 --- /dev/null +++ b/test-suite/misc/deps/αβ/γδ.v @@ -0,0 +1,4 @@ +Theorem simple : forall A, A -> A. +Proof. +auto. +Qed. diff --git a/test-suite/misc/deps/αβ/εζ.v b/test-suite/misc/deps/αβ/εζ.v new file mode 100644 index 000000000..e7fd25c0d --- /dev/null +++ b/test-suite/misc/deps/αβ/εζ.v @@ -0,0 +1 @@ +Require Import γδ. |