diff options
| author | Théo Zimmermann | 2020-04-24 14:39:22 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-24 17:03:00 +0200 |
| commit | 172c1c825061d450609468dd9c53974bfdb7d0cd (patch) | |
| tree | aa0c65da7e178e1c9bcda0fc95bb5529887b2a4d /dev/ci | |
| parent | 8c47247779b6db4c529510a7ce771162f54f5fbf (diff) | |
[dune] Fix dependencies of refman.
Dependencies specified through an alias do not trigger a rebuild when
they are modified. This is likely a Dune bug, but we still need to
fix this on our side as this is inconvenient.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions