diff --git a/share/dune b/share/dune index ecda8fe4361601e2d13a3e2fb9baf0377d3db79a..9a01f686a259debcc7c2c6ace9d62ce361be1d22 100644 --- a/share/dune +++ b/share/dune @@ -235,7 +235,6 @@ ; Analysis scripts (analysis-scripts/analysis.mk as analysis-scripts/analysis.mk) (analysis-scripts/benchmark_database.py as analysis-scripts/benchmark_database.py) -(analysis-scripts/benchmark.sh as analysis-scripts/benchmark.sh) (analysis-scripts/bench-sqlite.sh as analysis-scripts/bench-sqlite.sh) (analysis-scripts/build_callgraph.py as analysis-scripts/build_callgraph.py) (analysis-scripts/build.py as analysis-scripts/build.py)