diff options
| author | Hugo Herbelin | 2019-05-08 19:42:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | dd15e030be5e55d3770d27fbbc2fe0f5384f0166 (patch) | |
| tree | cff0290c690cec0acfc1ed67f90cdfba22748a36 /stm/asyncTaskQueue.ml | |
| parent | 26b7e819746a6b36d0e22181f64549c503fe0481 (diff) | |
Adding methods help and parse_extra to custom toplevels data.
In particular, method init does not do parsing any more.
This allows for instance to let coqidetop treats itself the
"-filteropts" option.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions