aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorErik Martin-Dorel2020-01-17 16:14:38 +0100
committerErik Martin-Dorel2020-01-17 16:14:38 +0100
commita7f4eb76935157112aa844b6c5ac29a36898235f (patch)
tree9bc84816f0dafed1bcdfad09dfc805d2f869d170
parent2646a263ba499f50ad09816ef76bea683517da26 (diff)
Revert "Don't run "opam clean -c" to workaround ocaml/opam#3828"
This reverts commit a03e0cb0ff40afabcaccba7f764076355ca82962.
-rw-r--r--Dockerfile2
-rw-r--r--Dockerfile.make2
2 files changed, 2 insertions, 2 deletions
diff --git a/Dockerfile b/Dockerfile
index eddbb0f..74ee396 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -29,7 +29,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
&& opam pin add -n -k path coq-mathcomp-field . \
&& opam pin add -n -k path coq-mathcomp-character . \
&& opam install -y -v -j ${NJOBS} coq-mathcomp-character \
- && opam clean -a -s --logs"]
+ && opam clean -a -c -s --logs"]
FROM coqorg/base:bare
diff --git a/Dockerfile.make b/Dockerfile.make
index 1a1dfc2..bb8b653 100644
--- a/Dockerfile.make
+++ b/Dockerfile.make
@@ -21,7 +21,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
&& opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \
&& opam update -y \
&& opam config list && opam repo list && opam list && coqc --version \
- && opam clean -a -s --logs \
+ && opam clean -a -c -s --logs \
&& sudo chown -R coq:coq /home/coq/mathcomp \
&& cd mathcomp \
&& make Makefile.coq \