From 9363107861e2702815b97bc71c8684d55f8f3274 Mon Sep 17 00:00:00 2001
From: Christian Grothoff <christian@grothoff.org>
Date: Wed, 13 Feb 2019 00:42:55 +0100
Subject: [PATCH] fixing 'make dist' issues

---
 src/util/Makefile.am | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 625ff87a2..fd00b077d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -41,7 +41,7 @@ if USE_COVERAGE
 endif
 
 if ENABLE_BENCHMARK
-  BENCHMARK = benchmark.c
+  BENCHMARK = benchmark.c benchmark.h
   PTHREAD = -lpthread
 endif
 
-- 
2.25.1