diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-21 13:13:34 +0000 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-21 13:18:13 +0000 |
commit | dd649afc99bf24c5f0864df50c4246046d5ac19b (patch) | |
tree | 5eb4a005115d086b391c39c686366ea802594f9a /.gitignore | |
parent | dbb7002920fac1bc0303dc1692fac71fc1139f11 (diff) |
Updated description of Make in README.md
Until now, because we didn't build the dependencies internally, it was
important for the pipeline to be usable with any version of Make. But
because of the new installation of dependencies (including GNU Make), that
is no longer the case. So we can safely use GNU Make and this needs to be
mentioned in `README.md'.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions