From 9f7c3301623aa11b1f4fc423c51710bd8f386696 Mon Sep 17 00:00:00 2001 From: Ben Harris Date: Wed, 6 May 2020 00:50:17 -0400 Subject: [PATCH] add navbar to wiki --- header.php | 11 +---------- nav.html | 9 +++++++++ wiki/Makefile | 4 ++-- 3 files changed, 12 insertions(+), 12 deletions(-) create mode 100644 nav.html diff --git a/header.php b/header.php index a3536bd..2e29d72 100644 --- a/header.php +++ b/header.php @@ -8,14 +8,5 @@ - +
diff --git a/nav.html b/nav.html new file mode 100644 index 0000000..0b6d865 --- /dev/null +++ b/nav.html @@ -0,0 +1,9 @@ + diff --git a/wiki/Makefile b/wiki/Makefile index 662a26f..3a5ffd5 100644 --- a/wiki/Makefile +++ b/wiki/Makefile @@ -14,6 +14,7 @@ index: dep-php index.html $(info building $@) @$(PANDOC) \ --from markdown+backtick_code_blocks \ + --include-before-body=../nav.html \ --template wiki.tmpl \ --lua-filter header-permalinks.lua \ --highlight-style=custom.theme \ @@ -36,8 +37,7 @@ index: dep-php index.html clean: $(info removing generated files) - -rm $(DST_HTML_FILES) - -rm $(DST_TXT_FILES) + -rm *.html *.txt dep-pandoc:: ifndef PANDOC