aboutsummaryrefslogtreecommitdiff
path: root/default.nix
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-11 15:03:43 +0200
committerMaxime Dénès2018-05-11 15:03:43 +0200
commit83b2e3430da9ba6d234a78c5b2910070c13d4152 (patch)
tree70004f9c65488a3cf4da850fcb1098547b872ade /default.nix
parentc3d719caf951e0c3716c85c8e3cf45f636d059eb (diff)
parent0e271d68a5bc6f5b8bc9a4ed2b9cf2faf283397e (diff)
Merge PR #7466: Remove tutorials from the repo
Diffstat (limited to 'default.nix')
-rw-r--r--default.nix4
1 files changed, 2 insertions, 2 deletions
diff --git a/default.nix b/default.nix
index 0b47942748..effee720de 100644
--- a/default.nix
+++ b/default.nix
@@ -90,9 +90,9 @@ stdenv.mkDerivation rec {
prefixKey = "-prefix ";
- buildFlags = optionals buildDoc [ "world" "sphinx" ];
+ buildFlags = [ "world" ] ++ optional buildDoc "doc-html";
- installTargets = [ "install" ] ++ optional buildDoc "install-doc-sphinx";
+ installTargets = [ "install" ] ++ optional buildDoc "install-doc-html";
inherit doCheck;