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 /src/scripts | |
| 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
Diffstat (limited to 'src/scripts')
| -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: |