aboutsummaryrefslogtreecommitdiff
path: root/doc/RecTutorial/RecTutorial.v
diff options
context:
space:
mode:
authorThéo Zimmermann2018-05-09 20:22:33 +0200
committerThéo Zimmermann2018-05-09 20:22:33 +0200
commit42c6b8f3b13cc5e974a129fe81481e64c9a8a182 (patch)
tree17f7ab4c276678b608477e35709088fba0c6379f /doc/RecTutorial/RecTutorial.v
parent9c56ba489abea0e1bfdebc5da9a77ba217de72fa (diff)
[travis] Add explicit opam switch command to guarantee we're using the requested compiler.
Diffstat (limited to 'doc/RecTutorial/RecTutorial.v')
0 files changed, 0 insertions, 0 deletions