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 /doc/tools/docgram/README.md | |
| parent | 8d1382b996d9421162839c3f481e866fef06fd41 (diff) | |
Add -no-update command line option to doc_grammar for Dune
Fix makefile glitches
Diffstat (limited to 'doc/tools/docgram/README.md')
| -rw-r--r-- | doc/tools/docgram/README.md | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 7ae98f4cd2..4cde3809f0 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -110,6 +110,9 @@ Other command line arguments: * `-no-warn` suppresses printing of some warning messages +* `-no-update` puts updates to `fullGrammar` and `orderedGrammar` into new files named + `*.new`, leaving the originals unmodified. For use in Dune. + * `-short` limits processing to updating/verifying only the `fullGrammar` file * `-verbose` prints more messages about the grammar |