diff options
| author | Dmitry Vyukov <dvyukov@google.com> | 2020-05-13 11:42:59 +0200 |
|---|---|---|
| committer | Dmitry Vyukov <dvyukov@google.com> | 2020-05-13 11:42:59 +0200 |
| commit | 9a6d42fb404b4433fa780d4258e394df8c96748d (patch) | |
| tree | cf94eeaea20efd43561bec9cc4af2eb0c7bb894c /executor | |
| parent | a44eb8f7eadcc16e73055948131b2c56b4fd5272 (diff) | |
Makefile: fix check_links
1. Disable pager.
2. Actually fail.
Diffstat (limited to 'executor')
0 files changed, 0 insertions, 0 deletions