aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMarc Coquand <marcc@fastmail.fr>2023-12-04 08:19:29 -0600
committerMarc Coquand <marcc@fastmail.fr>2023-12-04 08:19:29 -0600
commitce792e552d27e3c83251f11434795095dea7a93f (patch)
tree4a8539d59cd072c9f7e0dca0d4fc4811832f19a5
parentcf89e5ae5aade4a1bac676215289c9ee6db71b75 (diff)
downloadwormhole-ce792e552d27e3c83251f11434795095dea7a93f.tar.gz
wormhole-ce792e552d27e3c83251f11434795095dea7a93f.tar.bz2
wormhole-ce792e552d27e3c83251f11434795095dea7a93f.zip
Try again
-rw-r--r--.gitignore1
-rw-r--r--Dockerfile2
-rw-r--r--wormhole.opam34
3 files changed, 2 insertions, 35 deletions
diff --git a/.gitignore b/.gitignore
index 5c52b1f..b26b1d5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,6 +10,7 @@ _opam/
node_modules/
example/*/package-lock.json
+.wormhole.opam
# esy
_esy/
esy.lock
diff --git a/Dockerfile b/Dockerfile
index 93d745d..f158b0c 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -6,7 +6,7 @@ WORKDIR /home/opam
# Install dependencies
ADD wormhole.opam wormhole.opam
-RUN opam install . --deps-only
+RUN opam install . --deps-only --verbose
# Build project
ADD . .
diff --git a/wormhole.opam b/wormhole.opam
deleted file mode 100644
index 886447e..0000000
--- a/wormhole.opam
+++ /dev/null
@@ -1,34 +0,0 @@
-version: "4771982-dirty"
-# This file is generated by dune, edit dune-project instead
-opam-version: "2.0"
-version: "4771982-dirty"
-synopsis: "A short synopsis"
-description: "A longer description"
-maintainer: ["Maintainer Name"]
-authors: ["Author Name"]
-license: "LICENSE"
-tags: ["topics" "to describe" "your" "project"]
-homepage: "https://github.com/username/reponame"
-doc: "https://url/to/documentation"
-bug-reports: "https://github.com/username/reponame/issues"
-depends: [
- "ocaml"
- "dune" {>= "3.11"}
- "ppx_yojson_conv"
- "odoc" {with-doc}
-]
-build: [
- ["dune" "subst"] {dev}
- [
- "dune"
- "build"
- "-p"
- name
- "-j"
- jobs
- "@install"
- "@runtest" {with-test}
- "@doc" {with-doc}
- ]
-]
-dev-repo: "git+https://github.com/username/reponame.git"