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/deps | |
| parent | e9cd8ef01fe5b9ffc3e85984d0f9bc410a56f8ea (diff) | |
Adding a test for utf8 characters in directory names.
Diffstat (limited to 'test-suite/misc/deps')
| -rw-r--r-- | test-suite/misc/deps/αβ/γδ.v | 4 | ||||
| -rw-r--r-- | test-suite/misc/deps/αβ/εζ.v | 1 |
2 files changed, 5 insertions, 0 deletions
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 γδ. |