Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adjust 'make docs' to do an incremental build #16835

Merged
merged 6 commits into from Dec 14, 2020
Merged

Adjust 'make docs' to do an incremental build #16835

Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
cc06447
Update update-if-different to support copy mode
mppf Dec 8, 2020
f7a6dde
Update 'make docs' to be incremental
mppf Dec 9, 2020
36560dd
Better handle the case of a deleted file
mppf Dec 9, 2020
71f67d3
Fix typo in help message
mppf Dec 14, 2020
f0ac9e6
Add a comment to update-if-different
mppf Dec 14, 2020
5ae40a1
fix docs comment grammar
mppf Dec 14, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
11 changes: 11 additions & 0 deletions util/config/update-if-different
View file
Open in desktop
Expand Up @@ -53,6 +53,17 @@ def update(dst, src):
os.remove(src)

def copy(src, dst):
mppf marked this conversation as resolved.
Show resolved Hide resolved
""" copy src into dst.
The copy handles these two cases in a special way:
* If dst is a directory containing a file not in an src directory,
mppf marked this conversation as resolved.
Show resolved Hide resolved
that file will be removed.
* If dst contains a file that is the same as the file in src,
the file will not be copied (so that it is not "updated"
for follow-on build steps).
Additionally, this function handles the case where src is a file
and dst is a directory similarly to the 'cp' command.
"""

if not os.path.isdir(src):
# handle regular files

Expand Down