aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-07 16:21:10 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-07 09:22:22 +0200
commitb1cd93c7ad0f550077a62a1c7cb6915041c6c85e (patch)
treea71dde982168b8a6f4b09bad567d2b0217ea69ae /toplevel/usage.ml
parentfee2365f13900b4d4f4b88c986cbbf94403eeefa (diff)
Turning the printing primitive projection compatibility flag off by default.
Diffstat (limited to 'toplevel/usage.ml')
0 files changed, 0 insertions, 0 deletions