aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-08 14:19:38 +0100
committerGaëtan Gilbert2019-02-08 14:19:38 +0100
commit6e052101b827a0abef83bc6a54da83e30f70bc94 (patch)
treeded3aad25b447737045a5da97ca5bd60bea74bac /lib/flags.ml
parent95e723892c336808aad0926c675f3e0ac8ba7d99 (diff)
coqargs: use algebraic datatype for -native-compiler
Diffstat (limited to 'lib/flags.ml')
0 files changed, 0 insertions, 0 deletions