docs: add search widget to options page
Some checks are pending
Check for typos in the source tree / check-typos (push) Waiting to run

This commit is contained in:
raf 2024-12-09 10:27:01 +03:00
commit 37dc96575d
Signed by: NotAShelf
GPG key ID: AF26552424E53993
4 changed files with 62 additions and 2 deletions

View file

@ -62,7 +62,8 @@ in
# Copy anchor scripts to the script directory in document root.
cp -vt "$dest"/script \
${./static/script}/anchor-min.js \
${./static/script}/anchor-use.js
${./static/script}/anchor-use.js \
${./static/script}/search.js
substituteInPlace ./options.md \
--subst-var-by OPTIONS_JSON ./config-options.json
@ -100,6 +101,7 @@ in
--script highlightjs/loader.js \
--script script/anchor-use.js \
--script script/anchor-min.js \
--script script/search.js \
--toc-depth 2 \
--section-toc-depth 1 \
manual.md \