Opened 6 years ago
Closed 6 years ago
#20010 closed defect (fixed)
Delete empty directories in $SAGE_DOC
Reported by: | jdemeyer | Owned by: | |
---|---|---|---|
Priority: | blocker | Milestone: | sage-7.1 |
Component: | build | Keywords: | |
Cc: | hivert, mmezzarobba | Merged in: | |
Authors: | Jeroen Demeyer | Reviewers: | John Palmieri |
Report Upstream: | N/A | Work issues: | |
Branch: | cabdf45 (Commits, GitHub, GitLab) | Commit: | cabdf45dcc77c8732a13cf325a1c42293d10daae |
Dependencies: | Stopgaps: |
Description (last modified by )
In #19127, the automatic deleting of empty directories was removed, because of the mistaken assumption that it was not needed. While it's not needed in all cases, it is needed in one case:
it can happen that git checkout
leaves behind an empty directory (since it does not track directories), for example src/doc/en/reference/manifolds
. These directories should be deleted, otherwise Sphinx complains.
Change History (6)
comment:1 Changed 6 years ago by
- Dependencies set to #19127
comment:2 Changed 6 years ago by
- Branch set to u/jdemeyer/delete_empty_directories_in__sage_doc
comment:3 Changed 6 years ago by
- Commit set to cabdf45dcc77c8732a13cf325a1c42293d10daae
- Status changed from new to needs_review
comment:4 Changed 6 years ago by
- Dependencies #19127 deleted
- Description modified (diff)
comment:5 Changed 6 years ago by
- Reviewers set to John Palmieri
- Status changed from needs_review to positive_review
Looks good. With previous versions of docbuilding, there were many empty directories and so I objected to printing out the message Deleting empty directory ...
for each one. With this version, we should usually have just a few empty directories, if any, so it's fine to print it.
comment:6 Changed 6 years ago by
- Branch changed from u/jdemeyer/delete_empty_directories_in__sage_doc to cabdf45dcc77c8732a13cf325a1c42293d10daae
- Resolution set to fixed
- Status changed from positive_review to closed
New commits:
Delete empty directories in $SAGE_DOC before running Sphinx