From d982ccbe0230cf2a3fa06f9625ea1fc78607c1fd Mon Sep 17 00:00:00 2001 From: albert-github Date: Mon, 9 Oct 2023 13:09:46 +0200 Subject: [PATCH] Correcting stylesheet name The name `stylesheet.css` is replaced by a better name `cgal_stylesheet.css` a while ago, but apparently these 2 files were not updated. --- Documentation/doc/scripts/generate_how_to_cite.py | 2 +- Documentation/doc/scripts/html_output_post_processing.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Documentation/doc/scripts/generate_how_to_cite.py b/Documentation/doc/scripts/generate_how_to_cite.py index 71e1c6258c9..a891edddebc 100644 --- a/Documentation/doc/scripts/generate_how_to_cite.py +++ b/Documentation/doc/scripts/generate_how_to_cite.py @@ -85,7 +85,7 @@ pre_html=r""" - + CGAL ${CGAL_CREATED_VERSION_NUM} - Manual: Acknowledging CGAL diff --git a/Documentation/doc/scripts/html_output_post_processing.py b/Documentation/doc/scripts/html_output_post_processing.py index 9406785b508..90e8547eb58 100755 --- a/Documentation/doc/scripts/html_output_post_processing.py +++ b/Documentation/doc/scripts/html_output_post_processing.py @@ -70,7 +70,7 @@ def clean_doc(): duplicate_files=list(package_glob('./*/jquery.js')) duplicate_files.extend(package_glob('./*/dynsections.js')) duplicate_files.extend(package_glob('./*/resize.js')) - duplicate_files.extend(package_glob('./*/stylesheet.css')) + duplicate_files.extend(package_glob('./*/cgal_stylesheet.css')) # kill _all_, including the one in CGAL tabs.css files duplicate_files.extend(glob.glob('./*/tabs.css')) # left-over by doxygen?