diff options
| author | mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> | 2022-06-13 11:49:37 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-06-13 11:49:37 +0000 |
| commit | 118dd4ed0c901f56070052405f533d9deff5bb22 (patch) | |
| tree | a17da33db62ce591a05c2132c094913b371a41e0 /html-test/src/PruneWithWarning.hs | |
| parent | c5a83df91b97f85d995599c5ae7beacabe2ff040 (diff) | |
| parent | 3ab18cf06ae9392eab1349675dab8a177f1412da (diff) | |
Merge pull request #1108 from mpilgrem/fix783
Fix #783 Don't show button if --quickjump not present
Diffstat (limited to 'html-test/src/PruneWithWarning.hs')
0 files changed, 0 insertions, 0 deletions