From c132b5352784ea372156bd2fca5d71e088df0762 Mon Sep 17 00:00:00 2001
From: Robert Hensing <robert@roberthensing.nl>
Date: Mon, 4 Mar 2019 00:24:22 +0100
Subject: [PATCH] doc/manual: Update shell build

---
 doc/manual/.gitignore | 1 +
 doc/manual/build      | 2 ++
 2 files changed, 3 insertions(+)
 create mode 100755 doc/manual/build

diff --git a/doc/manual/.gitignore b/doc/manual/.gitignore
index 9ddf569..d0c7924 100644
--- a/doc/manual/.gitignore
+++ b/doc/manual/.gitignore
@@ -1,4 +1,5 @@
 introduction.xml
+installation.xml
 manual.html
 options-composition.xml
 options-service.xml
diff --git a/doc/manual/build b/doc/manual/build
new file mode 100755
index 0000000..67c9285
--- /dev/null
+++ b/doc/manual/build
@@ -0,0 +1,2 @@
+#!/usr/bin/env bash
+nix-shell -A manual --run 'patchPhase && make'