diff options
author | Jack Lloyd <[email protected]> | 2017-12-07 10:12:06 -0500 |
---|---|---|
committer | Jack Lloyd <[email protected]> | 2017-12-07 10:14:11 -0500 |
commit | 03d2d6057b2f2a3ce38c2af3bf18dadee684714f (patch) | |
tree | 7e6bc877a33833439abd3443f5ccd45cc2574dc2 | |
parent | 2ff5d004c95f69cc29a1ac832c29be4d411bc66a (diff) |
Remove the doc.stamp file in make clean target [ci skip]
Otherwise make docs followed by make clean leaves docs unbuilt
and make won't rebuild them. GH #1337
-rwxr-xr-x | src/scripts/cleanup.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/scripts/cleanup.py b/src/scripts/cleanup.py index 6dc7d2408..7660076dc 100755 --- a/src/scripts/cleanup.py +++ b/src/scripts/cleanup.py @@ -100,6 +100,8 @@ def main(args=None): dir_path = build_config[dir_type] remove_all_in_dir(dir_path) + remove_file(build_config['doc_stamp_file']) + try: shutil.rmtree(build_config['doc_output_dir']) except OSError: |