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'