diff options
| author | Théo Zimmermann | 2019-03-21 08:16:26 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-21 08:16:26 +0100 |
| commit | 5c0a7041cba6f2d2654ddc34a3c63a11f494d430 (patch) | |
| tree | bb898a867f2f85dbf71091d612cd7bad95ebd001 /dev/ci/ci-iris-lambda-rust.sh | |
| parent | 4a547c6aa58ef902c0a883d4be77761537a86280 (diff) | |
| parent | 314898447b30639e2c199aea32b41b0d42864d37 (diff) | |
Merge PR #9695: [make install] Do not install the sphinx doctrees
Reviewed-by: cpitclaudel
Ack-by: ejgallego
Diffstat (limited to 'dev/ci/ci-iris-lambda-rust.sh')
0 files changed, 0 insertions, 0 deletions