doc/manual: Update shell build

This commit is contained in:
Robert Hensing 2019-03-04 00:24:22 +01:00
parent cf562d6234
commit c132b53527
2 changed files with 3 additions and 0 deletions

View file

@ -1,4 +1,5 @@
introduction.xml introduction.xml
installation.xml
manual.html manual.html
options-composition.xml options-composition.xml
options-service.xml options-service.xml

2
doc/manual/build Executable file
View file

@ -0,0 +1,2 @@
#!/usr/bin/env bash
nix-shell -A manual --run 'patchPhase && make'