From 57d96e52f39dcceb294232bc674040af51ccc084 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Wed, 30 May 2018 15:15:41 +0100 Subject: [PATCH] Fix CMake macro Using ${CMAKE_SOURCE_DIR} doesn't work e.g. in a repository including cbmc as a subtree. Instead we use "${CBMC_SOURCE_DIR}/..". --- jbmc/regression/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt index 86037a4ff70..487dd801c66 100644 --- a/jbmc/regression/CMakeLists.txt +++ b/jbmc/regression/CMakeLists.txt @@ -1,4 +1,4 @@ -set(test_pl_path "${CMAKE_SOURCE_DIR}/regression/test.pl") +set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl") # For the best possible utilisation of multiple cores when # running tests in parallel, it is important that these directories are