diff options
| author | Théo Zimmermann | 2020-07-22 11:29:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-23 11:28:24 +0200 |
| commit | b7d501fb22e6725da20c59b895e19d30b6b2ad50 (patch) | |
| tree | 4653b6ec1754e3d6710c9953116a28560854ef88 /dev/ci | |
| parent | 56fd98a932f2700a63fe701bb71533fb48d6d06b (diff) | |
Ignore installation failure during call to brew.
Note that all the packages that we request are correctly installed and
the observed failure is independent (related to ruby which is not a
direct nor indirect dependency, only a dependency of brew itself).
The generated CoqIDE package has been tested and works correctly (with
no missing icon).
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions