diff options
| author | Fedja Beader <fedja@protonmail.ch> | 2024-05-10 21:45:26 +0000 |
|---|---|---|
| committer | Fedja Beader <fedja@protonmail.ch> | 2024-05-10 21:45:26 +0000 |
| commit | 46aed0c6b9be60355d89b4a9cf264f45290986b7 (patch) | |
| tree | 0d0902891c2858fe492187069664acbb838c0479 /src/gui | |
| parent | dd1627eb548a7705f749d2e8529207e6123e5e2e (diff) | |
| download | plus-46aed0c6b9be60355d89b4a9cf264f45290986b7.tar.gz plus-46aed0c6b9be60355d89b4a9cf264f45290986b7.tar.bz2 plus-46aed0c6b9be60355d89b4a9cf264f45290986b7.tar.xz plus-46aed0c6b9be60355d89b4a9cf264f45290986b7.zip | |
Download mplint release instead of recompiling every time
Saves 1min10s by not compiling and another 15s by moving it together with linters.
Squashed with:
* Make sure mplint internal error or failure to run is detected
* Make mplint breaking cause job to fail
* Move linters out of lightweight.. goes faster, 3m46s -> 1m45s
* Make script fail if any command returns nonzero or if any variable is
unset.
* Donwload mplint instead of building it
****
mana/plus!80
Diffstat (limited to 'src/gui')
0 files changed, 0 insertions, 0 deletions