From 98e2b048aa5419ac3d075e1d3f2499cb816fe92e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 11 Sep 2017 16:32:39 +0200
Subject: Adding a test for utf8 characters in directory names.

---
 test-suite/misc/deps-utf8.sh                            | 17 +++++++++++++++++
 .../misc/deps/\316\261\316\262/\316\263\316\264.v"      |  4 ++++
 .../misc/deps/\316\261\316\262/\316\265\316\266.v"      |  1 +
 3 files changed, 22 insertions(+)
 create mode 100755 test-suite/misc/deps-utf8.sh
 create mode 100644 "test-suite/misc/deps/\316\261\316\262/\316\263\316\264.v"
 create mode 100644 "test-suite/misc/deps/\316\261\316\262/\316\265\316\266.v"

(limited to 'test-suite/misc')

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/\316\261\316\262/\316\263\316\264.v" "b/test-suite/misc/deps/\316\261\316\262/\316\263\316\264.v"
new file mode 100644
index 000000000..f43a2d657
--- /dev/null
+++ "b/test-suite/misc/deps/\316\261\316\262/\316\263\316\264.v"
@@ -0,0 +1,4 @@
+Theorem simple : forall A, A -> A.
+Proof.
+auto.
+Qed.
diff --git "a/test-suite/misc/deps/\316\261\316\262/\316\265\316\266.v" "b/test-suite/misc/deps/\316\261\316\262/\316\265\316\266.v"
new file mode 100644
index 000000000..e7fd25c0d
--- /dev/null
+++ "b/test-suite/misc/deps/\316\261\316\262/\316\265\316\266.v"
@@ -0,0 +1 @@
+Require Import γδ.
-- 
cgit v1.2.3