diff options
| author |  Trevor Elliott <trevor@galois.com> | 2013-06-10 11:19:47 -0700 |
|---|---|---|
| committer | Trevor Elliott <trevor@galois.com> | 2013-06-10 11:19:47 -0700 |
| commit | 877520a9fa9020bfbcb10512b6b771f4491d3b9e (patch) | |
| tree | 7accf42fef67e1b5dcdd97a324ef72bae4521151 /doc | |
| parent | 686d00c01dc3096953156fa43daa164f1d59b7dc (diff) | |
Move more commands to Config.mk
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/build.mk | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/doc/build.mk b/doc/build.mk index f628a6c..79efa14 100644 --- a/doc/build.mk +++ b/doc/build.mk @@ -6,14 +6,12 @@ jsdoc-dir := $(build-dir)/jsdoc manual-dir := $(build-dir)/manual manual-src := $(path)/manual_src -pandoc := $(shell which pandoc 2>/dev/null) - # HTML Generation ############################################################## # Use pandoc to generate HTML quiet_cmd_pandoc = PANDOC $(call drop-prefix,$@) - cmd_pandoc = $(pandoc) $< -o $@ -s --highlight-style=kate \ + cmd_pandoc = $(pandoc-cmd) $< -o $@ -s --highlight-style=kate \ --template=$(manual-src)/template.html manual-deps := $(patsubst $(manual-src)/%.md,$(manual-dir)/%.html,\ @@ -25,10 +23,10 @@ $(manual-deps): $(manual-dir)/%.html: $(manual-src)/%.md | $(manual-dir) # HTML Manual ################################################################## -ifneq "$(pandoc)" "" +ifneq "$(pandoc-cmd)" "" doc: web-manual else -$(warning pandoc not found, not building the manual) +$(call strict-warning,pandoc not found, not building the manual) endif .PHONY: web-manual |