From 877520a9fa9020bfbcb10512b6b771f4491d3b9e Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Mon, 10 Jun 2013 11:19:47 -0700
Subject: Move more commands to Config.mk

---
 doc/build.mk | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3