diff options
| author | Emilio Jesus Gallego Arias | 2020-05-15 13:38:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-15 13:38:12 +0200 |
| commit | bcfb5f2cab54d0eb88ed57911b77c05d2b916431 (patch) | |
| tree | 1ca88bdd7fbd412386a2e0b4041f1929c9b55a75 /dev/tools | |
| parent | 959254ccd5c895782286dfb1d2c731e143e37d00 (diff) | |
| parent | 5383050ccdaca3f1b97e06bb782e5704231e9cdb (diff) | |
Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: ppedrot
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions