diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-01-31 05:22:31 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-09 23:02:59 +0100 |
| commit | 56ba2afe14a19bd0d396f89cab3ae720f2664be3 (patch) | |
| tree | 73a5ad4a3ee89559b78522c3fbc4ad14d17e0beb /stm/vernac_classifier.mli | |
| parent | 1222bc9e677c14884dd7c0f475003f01eb5fb1b1 (diff) | |
[toplevel] Refactor command line argument handling.
We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.
To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.
Diffstat (limited to 'stm/vernac_classifier.mli')
0 files changed, 0 insertions, 0 deletions