Fix compilation of Scope and Metrics
Showing
- src/plugins/metrics/dune 1 addition, 1 deletionsrc/plugins/metrics/dune
- src/plugins/metrics/register_gui.ml 21 additions, 21 deletionssrc/plugins/metrics/register_gui.ml
- src/plugins/scope/dune 3 additions, 3 deletionssrc/plugins/scope/dune
- src/plugins/scope/scope.mli 15 additions, 1 deletionsrc/plugins/scope/scope.mli
Loading
Please register or sign in to comment