diff options
| author | Gaëtan Gilbert | 2018-10-26 13:38:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-26 13:39:20 +0200 |
| commit | 8564e3c9ff59fd9815c8a77aa7e87fa552f8ac42 (patch) | |
| tree | 22d41e45180841521defc049af12c5b3bee4f20b /dev/dune_db | |
| parent | 48c837a0cd36c32d3149fc680c20c9119c7b13c2 (diff) | |
Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit."
This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc.
Should be merged before any PR with plugin tutorial overlays, or we
can just merge the vendor PR instead.
Diffstat (limited to 'dev/dune_db')
0 files changed, 0 insertions, 0 deletions