diff options
| author | Théo Zimmermann | 2020-02-13 08:52:34 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-13 08:52:34 +0100 |
| commit | 36a93a58446d487a136d999649d66ca7d4b09f70 (patch) | |
| tree | 2b0084e727fb1d5985174fa3ab2a745cda5ca70b | |
| parent | e9692a8ee7e9e71f64b93879bad6fc18c40d063f (diff) | |
| parent | bfa812b40138469ebe5bc3e306da79aa6b050e48 (diff) | |
Merge PR #11577: [nix] Fix building of the documentation
Reviewed-by: Zimmi48
| -rw-r--r-- | default.nix | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/default.nix b/default.nix index 174e199014..ae6a8d06e5 100644 --- a/default.nix +++ b/default.nix @@ -77,7 +77,7 @@ stdenv.mkDerivation rec { !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci" "nix"]) ./.; preConfigure = '' - patchShebangs dev/tools/ + patchShebangs dev/tools/ doc/stdlib ''; prefixKey = "-prefix "; |