diff options
| author | Théo Zimmermann | 2020-03-27 16:52:26 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-28 13:59:29 +0100 |
| commit | 89a2b709d254aeab2950764a89017cf8424ddfd1 (patch) | |
| tree | a6ce6b1f02c4bae2e834244ec9ec0d716a1d072e /kernel/type_errors.ml | |
| parent | 5f5f9520ccf0f107d381e5874a3743f47e37c409 (diff) | |
New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.
Use `dune build @check-gram --auto-promote` to automatically update
these two files. You will need to run it twice if the two files need
to be updated (which is the case most often) as Dune will stop after
the first diff failure.
The rst files are also updated but left in the `_build/` directory as
Dune wouldn't support targets outside the current directory. You can
just `mv _build/default/doc/sphinx doc` to update them after running
the @check-gram target.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions
