diff options
authorJulian Rüth <>2018-02-26 18:35:13 +0100
committerJulian Rüth <>2018-02-26 18:35:13 +0100
commit1bcb818963fd4fbbb02995a46222286233fb767a (patch)
parentSupport for funny characters in branch names (diff)
parentAllow user to override ARTIFACT_BASE on CircleCI (diff)
Merge branch 'ci' into binderu/saraedum/binder
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index d2dfc71..9f91b71 100644
--- a/Makefile
+++ b/Makefile
@@ -94,6 +94,8 @@ micro_release: bdist-clean sagelib-clean
find local/lib/python* -name '*.py' | while IFS= read -r fname; do [ -e "$${fname}c" -o -e "$${fname}o" ] && rm "$$fname"; done || true
@echo "Removing sphinx artifacts..."
rm -rf local/share/doc/sage/doctrees local/share/doc/sage/inventory
+ @echo "Removing documentation. Inspection in IPython still works."
+ rm -rf local/share/doc local/share/*/doc local/share/*/examples local/share/singular/html
@echo "Removing unnecessary files & directories - make will not be functional afterwards anymore"
@# We need src/sage/ for introspection with "??"
@# We need src/sage/bin/ for the scripts that invoke Sage