From 80c693a5af0a7cb61f88ecdb86c2b848cc3ce577 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Mon, 27 May 2019 13:46:49 +0200 Subject: [PATCH] Docker: don't clone ligo twice --- docker/Dockerfile | 1 - 1 file changed, 1 deletion(-) diff --git a/docker/Dockerfile b/docker/Dockerfile index 7363753bc..17bcd147c 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -20,7 +20,6 @@ RUN apt-get -y install \ m4 # Install ligo -RUN git clone https://gitlab.com/gabriel.alfour/ligo RUN opam update RUN cd ligo/src && \