aboutsummaryrefslogtreecommitdiff
path: root/dev/build
diff options
context:
space:
mode:
authorThéo Zimmermann2019-06-15 16:57:39 +0200
committerThéo Zimmermann2019-06-15 16:57:41 +0200
commitbf21ac7831ed2dc830ad66d1d6023e12dbb5dcaf (patch)
tree82945046f7a87a31fd2d42cee0b36afa8312901b /dev/build
parenta286c524a57597e6e29f17cdfa8c4af82cbb494c (diff)
[dune] Install .byte version of coqidetop like for coqtop.
Diffstat (limited to 'dev/build')
0 files changed, 0 insertions, 0 deletions