diff options
| author | Jim Fehrle | 2020-03-29 10:50:51 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-03-29 13:30:13 -0700 |
| commit | 511134687d89fa5a5a5bbf45f40fa8ed615097d3 (patch) | |
| tree | 3ec4999b8c5dc16ed27b7047c819933798951ffe /plugins/syntax | |
| parent | 8d1382b996d9421162839c3f481e866fef06fd41 (diff) | |
Add -no-update command line option to doc_grammar for Dune
Fix makefile glitches
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions