1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Description: Disable version-select dropdown menu in html documentation
Only makes sense if we have multiple versions of the documentation installed,
which will not be the case. This only matters when the documentation is
viewed over a local webserver, e.g., when using dwww.
Author: Doug Torrance <dtorrance@debian.org>
Forwarded: not-needed
Last-Update: 2023-10-03
--- a/M2/Macaulay2/m2/html.m2
+++ b/M2/Macaulay2/m2/html.m2
@@ -56,8 +56,6 @@
defaultHEAD = title -> HEAD splice { TITLE title, defaultCharset(), defaultStylesheet(), KaTeX(),
SCRIPT {"src" => getStyleFile "prism.js", ""},
- SCRIPT {"var current_version = '", version#"VERSION", "';"},
- SCRIPT {"src" => getStyleFile "version-select.js"},
LINK {
"rel" => "icon", "type" => "image/x-icon",
"href" => getStyleFile "icon.gif"}}
|
