diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-01-10 12:32:15 +0000 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-01-10 12:36:52 +0000 |
| commit | adb4ae4e2da2591cf82886c205044cb901498019 (patch) | |
| tree | 30b13e9ecd23a6f6292a8d8d0b1def1af91a3c1d /reproduce/src/make/paper.mk | |
| parent | e557699b996b906202ecdf2fa2e29f62a3cfd88a (diff) | |
cURL added as a dependency of Git
Git needs cURL in its build. Until now, by chance cURL was always built
before Git, but while building this pipeline on a system, Git was built
before cURL and we found the problem.
I also noticed that we hadn't added `Your name <your@email.address>' to the
`for-group' script. This has been corrected now.
Diffstat (limited to 'reproduce/src/make/paper.mk')
0 files changed, 0 insertions, 0 deletions