diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-11 16:32:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-13 19:00:42 +0200 |
| commit | 98e2b048aa5419ac3d075e1d3f2499cb816fe92e (patch) | |
| tree | 632d80faab6f3f39ce89aa5cf68d2b277dd4e495 /test-suite/misc | |
| parent | e9cd8ef01fe5b9ffc3e85984d0f9bc410a56f8ea (diff) | |
Adding a test for utf8 characters in directory names.
Diffstat (limited to 'test-suite/misc')
| -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 γδ. |