diff options
author | Raul Infante-Sainz <infantesainz@gmail.com> | 2019-02-28 12:54:29 +0000 |
---|---|---|
committer | Raul Infante-Sainz <infantesainz@gmail.com> | 2019-02-28 12:54:29 +0000 |
commit | 4f50f0acf3e06f6a1ade0532df0b95a39c23629a (patch) | |
tree | ba74cb5e6b2ce0356e90cffc5d24e7bda0fdb80a /reproduce/analysis/make | |
parent | 69a780ef770034e69db96c2e1e8a4d83626a4d2f (diff) |
GNU GCC is now in the pipeline
Until now, the pipeline was not installing its own `gcc' but using the
system one by making a symbolic link.
With this commit, GNU GCC has been added into the pipeline. Right now
the installation does not work on Mac OS system beause of some conflicts
with `clang', but in principle it should work on GNU Linux distributions.
Diffstat (limited to 'reproduce/analysis/make')
0 files changed, 0 insertions, 0 deletions