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 d34d6ebfecbab8c32da1e591e5604bef41f9650b..000d0e50bcb2af2531df66e4a9188b3438cad272 100644 (file)
--- 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("")