diff options
| author | Pamplemousse <xav.maso@gmail.com> | 2021-08-04 19:44:12 -0700 |
|---|---|---|
| committer | Pamplemousse <xav.maso@gmail.com> | 2021-08-04 19:47:05 -0700 |
| commit | de39cfb9f39603c61092f01482cb105349187fc6 (patch) | |
| tree | 2a8b24fc2ab618bd73b69683dba34b95a1adb38b | |
| parent | 1f930841495548b5e111946819b84bf9a10f47a9 (diff) | |
doc/manual: don't need to copy `highlight.js` manually
Signed-off-by: Pamplemousse <xav.maso@gmail.com>
| -rw-r--r-- | doc/manual/local.mk | 1 | ||||
| -rw-r--r-- | doc/manual/theme/highlight.js (renamed from doc/manual/highlight.pack.js) | 0 |
2 files changed, 0 insertions, 1 deletions
diff --git a/doc/manual/local.mk b/doc/manual/local.mk index e25157af8..c4cedc810 100644 --- a/doc/manual/local.mk +++ b/doc/manual/local.mk @@ -86,6 +86,5 @@ install: $(d)/src/command-ref/new-cli $(docdir)/manual/index.html: $(MANUAL_SRCS) $(d)/book.toml $(d)/custom.css $(d)/src/SUMMARY.md $(d)/src/command-ref/new-cli $(d)/src/command-ref/conf-file.md $(d)/src/expressions/builtins.md $(trace-gen) RUST_LOG=warn mdbook build doc/manual -d $(docdir)/manual - @cp doc/manual/highlight.pack.js $(docdir)/manual/highlight.js endif diff --git a/doc/manual/highlight.pack.js b/doc/manual/theme/highlight.js index fba8b4a5a..fba8b4a5a 100644 --- a/doc/manual/highlight.pack.js +++ b/doc/manual/theme/highlight.js |