diff options
| author |  Erik Martin-Dorel <erik@martin-dorel.org> | 2018-03-07 18:27:24 +0100 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2018-03-07 18:27:24 +0100 |
| commit | 315b7043953449fd6d982b01e4bcda91bb37ae7e (patch) | |
| tree | def7d96a776f06d6ee7e1df53366e72ecf1f209a /Makefile.travis | |
| parent | 23e480368e6952e10c084b627f7e39c60e0daf02 (diff) | |
| parent | e1b3efb8e8ace78af9a0459318a927a28574c92e (diff) | |
Merge pull request #344 from ProofGeneral/font-lock-fix
Add a missing parameter in advice on font-lock-fontify-keywords-region
Diffstat (limited to 'Makefile.travis')
0 files changed, 0 insertions, 0 deletions