diff options
| author | Emilio Jesus Gallego Arias | 2018-10-09 20:35:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-24 17:57:33 +0100 |
| commit | 7a786e80042ab2b89e5f078bc5143c74e72f14e3 (patch) | |
| tree | 5a0276c5203698dc5b006b26cecc1ddeb7c119f9 /kernel | |
| parent | e0f55aecee2ed9fc6f56979c255688e08b136c20 (diff) | |
[toplevel] Move command line path processing to Coqargs
We move the processing of path-related arguments to `Coqargs`, and
following experience from `SerAPI` we stored already-processed
`coq_paths` in the `opts` record.
This has proven to be very convenient as to avoid duplication of code
in the presence of several clients of the `Coqargs` parsing
functionality.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions