[Metrics] use Filepath parameters for relevant options
Showing
- src/plugins/metrics/metrics_acsl.ml 4 additions, 3 deletionssrc/plugins/metrics/metrics_acsl.ml
- src/plugins/metrics/metrics_base.ml 4 additions, 3 deletionssrc/plugins/metrics/metrics_base.ml
- src/plugins/metrics/metrics_base.mli 1 addition, 1 deletionsrc/plugins/metrics/metrics_base.mli
- src/plugins/metrics/metrics_cilast.ml 4 additions, 3 deletionssrc/plugins/metrics/metrics_cilast.ml
- src/plugins/metrics/metrics_parameters.ml 3 additions, 1 deletionsrc/plugins/metrics/metrics_parameters.ml
- src/plugins/metrics/metrics_parameters.mli 1 addition, 1 deletionsrc/plugins/metrics/metrics_parameters.mli
Loading
Please register or sign in to comment