Fix cd in coq-stdlib.dev

Co-authored-by: Guillaume Melquiond <[email protected]>
proux01 · Dec 7, 2024 · 93bf38d · 93bf38d
1 parent 25d2146
commit 93bf38d
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
@@ -29,7 +29,7 @@ depends: [
 depopts: ["coq-native"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
-  ["cd" "stdlib"]
+  ["sh" "-c" "echo '(dirs stdlib)' > dune"]
   ["dune" "subst"] {dev}
   [
     "dune"
@@ -43,7 +43,7 @@ build: [
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
-  ["dune" "install" "--root" "." "-p" name "--create-install-files" name]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 
 url {