diff options
Diffstat (limited to 'repo/www/make-deps.py')
| -rwxr-xr-x | repo/www/make-deps.py | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/repo/www/make-deps.py b/repo/www/make-deps.py index 4045580..4ca4e6e 100755 --- a/repo/www/make-deps.py +++ b/repo/www/make-deps.py @@ -37,7 +37,6 @@ def html_path(source_path, top_dir, out_dir): def write_dependencies(output, sources, top_dir, out_dir): pages = [] - directories = set() for src in sources: html = html_path(src, top_dir, out_dir) @@ -46,11 +45,9 @@ def write_dependencies(output, sources, top_dir, out_dir): print(f'{html}: {src} | {html_dir}', file=output) pages.append(html) - directories.add(html_dir) print(file=output) print(f'pages = {" ".join(pages)}', file=output) - print(f'page_folders = {" ".join(directories)}', file=output) def main(argv): |