From 83fd07f18c450dba0699ebbe4a3fb05d5fd8776a Mon Sep 17 00:00:00 2001
From: Mark Nunberg <mnunberg@haskalah.org>
Date: Sun, 3 Mar 2019 18:10:04 +0200
Subject: [PATCH] get_deps: use `deps` directory by default rather than
 platform specific

one
---
 .circleci/config.yml | 2 +-
 get_deps.sh          | 6 +-----
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 5a1854859..b52a759a4 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -26,7 +26,7 @@ jobs:
             sudo ln -s /home/circleci/project/cmake-bin/bin/cmake /usr/local/bin/cmake
             echo `cmake --version`
             rm -rf /home/circleci/project/deps
-            DEPS_DIRECTORY=deps bash get_deps.sh cpu
+            bash get_deps.sh cpu
             git clone git://github.com/antirez/redis.git --branch 5.0
             (cd redis && make malloc=libc -j4 && sudo make install)
 
diff --git a/get_deps.sh b/get_deps.sh
index 3d430c1c6..3a8e0c799 100755
--- a/get_deps.sh
+++ b/get_deps.sh
@@ -5,13 +5,9 @@ set -x
 BASE_DIRECTORY=`pwd`
 
 # Allow different deps for different platforms:
-PLATNAME=${OSTYPE}
-if [ -e /etc/debian-version ]; then
-    PLATNAME=${PLATNAME}-deb
-fi
 
 if [ -z "$DEPS_DIRECTORY" ]; then
-  DEPS_DIRECTORY=${BASE_DIRECTORY}/deps-${PLATNAME}
+  DEPS_DIRECTORY=${BASE_DIRECTORY}/deps
 fi
 
 mkdir -p ${DEPS_DIRECTORY}