script/make_rocksdb_makefile.sh: do not include rocksdb/tools/rdb/*

Fixes: http://tracker.ceph.com/issues/13554
Signed-off-by: Kefu Chai <kchai@redhat.com>

diff --git a/src/script/make_rocksdb_makefile.sh b/src/script/make_rocksdb_makefile.sh
index bd8816df79302e5cb7161b6cc140e4dac60b4064..4f614c916ca95330844a233a4a7c31ec821887b9 100755 (executable)
--- 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/$$