diff options
| author | Théo Zimmermann | 2018-05-09 20:22:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-09 20:22:33 +0200 |
| commit | 42c6b8f3b13cc5e974a129fe81481e64c9a8a182 (patch) | |
| tree | 17f7ab4c276678b608477e35709088fba0c6379f /doc/RecTutorial | |
| parent | 9c56ba489abea0e1bfdebc5da9a77ba217de72fa (diff) | |
[travis] Add explicit opam switch command to guarantee we're using the requested compiler.
Diffstat (limited to 'doc/RecTutorial')
0 files changed, 0 insertions, 0 deletions