.ci/write-dockerfile.sh: Remove duplicated ADD

kryzar · Jun 4, 2024 · d068c8d · d068c8d
1 parent 8d0c849
commit d068c8d
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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; \