diff options
| author | Gaëtan Gilbert | 2019-04-01 14:15:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-16 15:11:03 +0100 |
| commit | 1e1fd6d7e66cee0130a119bf1ded6b7dee17131c (patch) | |
| tree | dec256271cc14e401b358953867ba05e74fecae7 /plugins | |
| parent | 839ed4e80ca4dc068422c7c9fdb0c00e4ff1ebab (diff) | |
Command-line setters for options
TODO coqproject handling (for now it can be done through -arg I guess)
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions