aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorThomas Letan2020-07-29 14:53:19 +0200
committerThomas Letan2020-07-29 17:48:22 +0200
commitce233d5b4a6f8d506c37a2a492679a66f9618a94 (patch)
tree6e3397d7820edfe44c6266d0ff613ff5c2871e45 /kernel/genOpcodeFiles.ml
parent827d430fc5645bf5ad12d0a7fc6298b56ccce5f0 (diff)
coqdoc: Fix the “details” environment
The change introduced by 41a1d66 has broken the feature prior to its initial release. We attempt to fix the issue, and add a comment to warn feature developers in order to avoid facing the same issue again.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions