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.
This commit is contained in:
albert-github 2023-10-09 13:09:46 +02:00
parent 8a4b492f1c
commit d982ccbe02
2 changed files with 2 additions and 2 deletions

View File

@ -85,7 +85,7 @@ pre_html=r"""<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "htt
<link rel="icon" type="image/png" href="../Manual/g-196x196-doc.png"/>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<link href="stylesheet.css" rel="stylesheet" type="text/css" />
<link href="cgal_stylesheet.css" rel="stylesheet" type="text/css" />
<title>CGAL ${CGAL_CREATED_VERSION_NUM} - Manual: Acknowledging CGAL</title>
</head>
<body>

View File

@ -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?