From 433e60f876a804fbe05aa017b14a2169d04974cb Mon Sep 17 00:00:00 2001
From: Ciro Santilli <ciro.santilli@gmail.com>
Date: Thu, 16 Aug 2018 17:42:46 +0100
Subject: [PATCH] common: common_gem5_default_src_dir factor out

---
 common | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/common b/common
index c8d1d62..b9dcd05 100644
--- a/common
+++ b/common
@@ -122,7 +122,7 @@ common_setup() {
   if [ -n "$common_gem5_worktree" ]; then
     common_gem5_src_dir="${common_gem5_non_default_src_root_dir}/${common_gem5_worktree}"
   else
-    common_gem5_src_dir="${common_root_dir}/gem5/gem5"
+    common_gem5_src_dir="$common_gem5_default_src_dir"
   fi
   if "$common_gem5"; then
     common_exec="$common_gem5_exec"