From 4593ac048f355856232482bdc4964ce90d64169b Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Fri, 5 Jun 2020 03:18:16 +0100 Subject: [PATCH] If using 'ninja', tell the user to run 'ninja' not 'make' (#4568) ## Issue If you call CVC4's `configure` script with `--ninja`, then you get a misleading status message: ``` [avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5 Now change to 'build' and type make, followed by make check or make install. -- Configuring done -- Generating done -- Build files have been written to: /home/avj/working/CVC4/build ``` ## Solution This commit simply fixes the status message to tell the user to run the correct command based on the specified generator: ``` [avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5 Now change to 'build' and type 'ninja', followed by 'ninja check' or 'ninja install'. -- Configuring done -- Generating done -- Build files have been written to: /home/avj/working/CVC4/build ``` Signed-off-by: Andrew V. Jones --- CMakeLists.txt | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d34d6ebfe..000d0e50b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -719,6 +719,14 @@ else() ) endif() +if("${CMAKE_GENERATOR}" STREQUAL "Ninja") + set(BUILD_COMMAND_NAME "ninja") +else() + set(BUILD_COMMAND_NAME "make") +endif() + message("") -message("Now just type make, followed by make check or make install.") +message("Now just type '${BUILD_COMMAND_NAME}', " + "followed by '${BUILD_COMMAND_NAME} check' " + "or '${BUILD_COMMAND_NAME} install'.") message("") -- 2.30.2