diff options
author | Eelco Dolstra <edolstra@gmail.com> | 2020-12-04 15:02:37 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-04 15:02:37 +0100 |
commit | 45645b6f3b6c45f20a7bece6da395c3e095aedd0 (patch) | |
tree | ef5efb1825a82bd04f0f8c7f7efb52f10d05d679 /configure.ac | |
parent | d94239c9794b3467cbbde11ff8634e15111feaae (diff) | |
parent | 5f66edf24503fabf410bb923de761131cea57771 (diff) |
Merge pull request #4314 from tweag/less-noisy-make-doc
Make `make install` less noisy
Diffstat (limited to 'configure.ac')
0 files changed, 0 insertions, 0 deletions