diff --git a/tools/docker/manylinux1.Dockerfile b/tools/docker/manylinux1.Dockerfile index 9c63b2cfff..245e3bbf1f 100644 --- a/tools/docker/manylinux1.Dockerfile +++ b/tools/docker/manylinux1.Dockerfile @@ -32,6 +32,10 @@ RUN ./configure --prefix=/usr RUN make RUN make install +RUN git clone https://github.com/google/or-tools /root/or-tools +WORKDIR /root/or-tools +RUN make third_party + ADD build-manylinux1.sh /root WORKDIR /root