Merge PR #12350: [test-suite] Ensure copies of files are writable

Reviewed-by: SkySkimmer

1 files changed, 15 insertions, 7 deletions

diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index 30be5e6456..ab89e12592 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -9,10 +9,18 @@ cd _test || exit 1
 mkdir -p src
 mkdir -p theories/sub
 
-cp ../../template/theories/sub/testsub.v theories/sub
-cp ../../template/theories/test.v theories
-cp ../../template/src/test.mlg src
-cp ../../template/src/test_aux.mli src
-cp ../../template/src/test.mli src
-cp ../../template/src/test_plugin.mlpack src
-cp ../../template/src/test_aux.ml src
+cp_file() {
+  local _TARGET=$1
+  cp ../../template/$_TARGET $_TARGET
+  chmod u+w $_TARGET
+}
+
+# We chmod +w as to fix the case where the sources are read-only, as
+# for example when using Dune's cache.
+cp_file theories/sub/testsub.v
+cp_file theories/test.v
+cp_file src/test.mlg
+cp_file src/test_aux.mli
+cp_file src/test.mli
+cp_file src/test_plugin.mlpack
+cp_file src/test_aux.ml