From 6be8f8dd59b910642dcb660be3b8eadbcb8dbcea Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 3 Jun 2022 16:19:00 +0200
Subject: [PATCH] [install] removed benchmark in share

---
 share/dune | 1 -
 1 file changed, 1 deletion(-)

diff --git a/share/dune b/share/dune
index ecda8fe4361..9a01f686a25 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)
-- 
GitLab