From d068c8dcc82e667006ecd298a761aff8335a3654 Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Tue, 4 Jun 2024 15:09:09 -0700 Subject: [PATCH] .ci/write-dockerfile.sh: Remove duplicated ADD --- .ci/write-dockerfile.sh | 1 - 1 file changed, 1 deletion(-) diff --git a/.ci/write-dockerfile.sh b/.ci/write-dockerfile.sh index ffdfa5404f6..beee1440368 100755 --- a/.ci/write-dockerfile.sh +++ b/.ci/write-dockerfile.sh @@ -339,7 +339,6 @@ ENV SAGE_CHECK=warn ENV SAGE_CHECK_PACKAGES="!cython,!r,!python3,!gap,!cysignals,!linbox,!git,!ppl,!cmake,!rpy2,!sage_sws2rst" $ADD .gitignore /new/.gitignore $ADD src /new/src -ADD .ci /.ci RUN cd /new && rm -rf .git && \ if /.ci/retrofit-worktree.sh worktree-pre /sage; then \ cd /sage && touch configure build/make/Makefile; \