From cbc3089aed52763af04cd56c2e811f1d418bcff6 Mon Sep 17 00:00:00 2001 From: Kefu Chai Date: Wed, 15 Jun 2016 11:25:27 +0800 Subject: [PATCH] script/make_rocksdb_makefile.sh: do not include rocksdb/tools/rdb/* Fixes: http://tracker.ceph.com/issues/13554 Signed-off-by: Kefu Chai --- src/script/make_rocksdb_makefile.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/script/make_rocksdb_makefile.sh b/src/script/make_rocksdb_makefile.sh index bd8816df7930..4f614c916ca9 100755 --- a/src/script/make_rocksdb_makefile.sh +++ b/src/script/make_rocksdb_makefile.sh @@ -4,7 +4,7 @@ cd rocksdb git clean -dffx cd .. echo "EXTRA_DIST += \\" > /tmp/$$ -for f in `find rocksdb -type f | grep -v /.git$ | sort`; do +for f in `find rocksdb -type f | grep -v -e /.git$ -e ^rocksdb/tools/rdb | sort`; do echo " $f \\" >> /tmp/$$ done echo " rocksdb/AUTHORS" >> /tmp/$$ -- 2.47.3