Verified Commit d88a6de4 authored by Ansgar Burchardt's avatar Ansgar Burchardt
Browse files

Use new path /duneci instead of /dune.

parent 4ea2c0f3
Pipeline #31 skipped
FROM duneci/dune:2.4
RUN mkdir modules
RUN mkdir -p modules
WORKDIR /dune/modules
WORKDIR /duneci/modules
RUN git clone -b releases/2.4-1
RUN git clone -b releases/2.4-compatible
RUN git clone
RUN git clone -b releases/2.4
RUN dunecontrol all
ENV DUNE_CONTROL_PATH=.:/dune/modules
WORKDIR /duneci
ENV DUNE_CONTROL_PATH=.:/duneci/modules
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment