From: Andrew V. Jones <andrew.jones@vector.com>
Date: Fri, 5 Jun 2020 02:18:16 +0000 (+0100)
Subject: If using 'ninja', tell the user to run 'ninja' not 'make' (#4568)
X-Git-Tag: cvc5-1.0.0~3253
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4593ac048f355856232482bdc4964ce90d64169b;p=cvc5.git

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 <andrew.jones@vector.com>
---

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("")