Merge pull request #3246 from proux01/fix_stdlib_dev

[core-dev] Fix installation of coq-stdlib.dev
coq · Dec 9, 2024 · 296f08c · 296f08c
2 parents e1cb24f + 5285be9
commit 296f08c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
@@ -38,12 +38,12 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
-  ["dune" "install" "-p" name "--create-install-files" name]
+  ["dune" "install" name]
+  ["sh" "-c" "echo 'From Stdlib Require Import Reals.' > test.v && coqc test.v"] {with-test}
 ]
 
 url {