copy dist files to _dist directory

goblint · Dec 8, 2023 · ed75229 · ed75229
1 parent 61fcbbe
commit ed75229
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/make.sh b/make.sh
@@ -37,7 +37,10 @@ rule() {
       eval $(opam config env)
       dune build gobview &&
       rm -f goblint-http &&
-      cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http
+      cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http &&
+      rm -rf gobview/_dist &&
+      mkdir gobview/_dist
+      cp ./_build/default/gobview/dist/* gobview/_dist/
     # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable
     ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html
       dune build $TARGET.bc.js &&