From de39cfb9f39603c61092f01482cb105349187fc6 Mon Sep 17 00:00:00 2001 From: Pamplemousse Date: Wed, 4 Aug 2021 19:44:12 -0700 Subject: [PATCH] doc/manual: don't need to copy `highlight.js` manually Signed-off-by: Pamplemousse --- doc/manual/local.mk | 1 - doc/manual/{highlight.pack.js => theme/highlight.js} | 0 2 files changed, 1 deletion(-) rename doc/manual/{highlight.pack.js => theme/highlight.js} (100%) 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 similarity index 100% rename from doc/manual/highlight.pack.js rename to doc/manual/theme/highlight.js