diff options
| author | Emilio Jesus Gallego Arias | 2020-02-05 12:53:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:24:53 +0100 |
| commit | fe6d6e9ab1291a03e5fe68287b90ee1b244e8f2d (patch) | |
| tree | fe8cb673c25933481965df0b62301e0e0b71d493 /kernel/float64.mli | |
| parent | adf04f62d3ff5b0651cec2e8596ce3900d3af1eb (diff) | |
[coqdep] Remove dumpgraph and broken options
We remove the `dumpgraph` option which was causing quite a bit of
duplication, we also clean up options marked as broken `-w/-D`
Diffstat (limited to 'kernel/float64.mli')
0 files changed, 0 insertions, 0 deletions