diff options
| author | Andrew V. Jones <andrew.jones@vector.com> | 2020-06-05 03:18:16 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-04 19:18:16 -0700 |
| commit | 4593ac048f355856232482bdc4964ce90d64169b (patch) | |
| tree | 0dbf5238c54c8e01093eda0b369716d6ecd277fd | |
| parent | a2fc412f22552ae0e8f9c36650d1de2d362638dd (diff) | |
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>
| -rw-r--r-- | CMakeLists.txt | 10 |
1 files changed, 9 insertions, 1 deletions
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("") |