aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorEnrico Tassi2020-09-18 13:59:30 +0200
committerEnrico Tassi2020-09-18 13:59:30 +0200
commit2b258e90df02448341c051ac21b84cf1c7c20428 (patch)
tree7d16f7030e9b1d96be23ae27811195e376354465 /test-suite
parentff508baf8de691dfa94b9d65d7c77cf395127381 (diff)
[lib] make canonical_path_name always absolute (fix #13031)
Diffstat (limited to 'test-suite')
-rwxr-xr-xtest-suite/misc/coq_makefile_destination_of.sh26
1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/misc/coq_makefile_destination_of.sh b/test-suite/misc/coq_makefile_destination_of.sh
new file mode 100755
index 0000000000..fc8e089ccf
--- /dev/null
+++ b/test-suite/misc/coq_makefile_destination_of.sh
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+TMP=`mktemp -d`
+cd $TMP
+
+function assert_eq() {
+ if [ "$1" != "$2" ]; then
+ echo "coq_makefile generates destination" $1 "!=" $2
+ cd /
+ rm -rf $TMP
+ exit 1
+ fi
+}
+
+assert_eq `coq_makefile -destination-of src/Y/Z/Test.v -Q src X` "X//Y/Z"
+mkdir src
+assert_eq `coq_makefile -destination-of src/Y/Z/Test.v -Q src X` "X//Y/Z"
+mkdir -p src/Y/Z
+touch src/Y/Z/Test.v
+assert_eq `coq_makefile -destination-of src/Y/Z/Test.v -Q src X` "X//Y/Z"
+cd /
+rm -rf $TMP
+exit 0