Fix issues with Ninja build system and add configure option. (#3166)

Adds option --ninja to configure.sh.

1 files changed, 5 insertions, 0 deletions

diff --git a/configure.sh b/configure.sh
index 9bf33ae8a..d7e807c65 100755
--- a/configure.sh
+++ b/configure.sh
@@ -20,6 +20,7 @@ General options;
   --best                   turn on dependencies known to give best performance
   --gpl                    permit GPL dependencies, if available
   --win64                  cross-compile for Windows 64 bit
+  --ninja                  use Ninja build system
 
 
 Features:
@@ -117,6 +118,7 @@ drat2er=default
 dumping=default
 gpl=default
 win64=default
+ninja=default
 glpk=default
 lfsc=default
 muzzle=default
@@ -217,6 +219,8 @@ do
     --win64) win64=ON;;
     --no-win64) win64=OFF;;
 
+    --ninja) ninja=ON;;
+
     --glpk) glpk=ON;;
     --no-glpk) glpk=OFF;;
 
@@ -357,6 +361,7 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
 [ $win64 != default ] \
   && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
+[ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
 [ $optimized != default ] \