aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2019-02-16 16:42:52 +0100
committerGaëtan Gilbert2019-02-19 13:07:13 +0100
commit499491f8efd3a02dacb64c779edc246510b1d35f (patch)
tree04acdbeade11b3207d743c24ff039bda33d2caae /kernel/genOpcodeFiles.ml
parentb16cea4007e4286d596a46bce80815939bca271d (diff)
[sphinx] Refactor handling of options for coqtop directive.
Make it mandatory to give exactly one display option.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions