diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-19 06:18:14 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-22 18:46:27 +0200 |
commit | 323af0fd83d1d23c9b0324b19f2fa542419653ab (patch) | |
tree | 0b6046e3be916c57b1c6cb7228439e225d28b397 /plugins/romega/const_omega.mli | |
parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) |
Removing TODO file which is unused for more than 10 years.
Hoping this is ok for everyone, otherwise we can discuss about it.
Diffstat (limited to 'plugins/romega/const_omega.mli')
0 files changed, 0 insertions, 0 deletions