diff options
| author | Eelco Dolstra <edolstra@gmail.com> | 2021-08-05 15:13:07 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-05 15:13:07 +0200 |
| commit | d64f9671fcce47e792974b372dc72de8c49994b7 (patch) | |
| tree | 5ff35626e9472c07027bed709ffe8a49af397f15 | |
| parent | 47e96bb533f8cacc171bec9b688b134de31a48a9 (diff) | |
| parent | de39cfb9f39603c61092f01482cb105349187fc6 (diff) | |
Merge pull request #5094 from Pamplemousse/simpler_doc
doc/manual: don't need to copy `highlight.js` manually
| -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 dd1d5f0fa..93ec3cad0 100644 --- a/doc/manual/local.mk +++ b/doc/manual/local.mk @@ -96,6 +96,5 @@ doc/manual/generated/man1/nix3-manpages: $(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 |