diff --git a/.gitignore b/.gitignore index a935d9dba..77f4d1896 100644 --- a/.gitignore +++ b/.gitignore @@ -44,7 +44,6 @@ bld_rel_x64/* # Auto generated files. config.log config.status -configure install_tactic.cpp mem_initializer.cpp gparams_register_modules.cpp diff --git a/configure b/configure new file mode 100755 index 000000000..29408d3e7 --- /dev/null +++ b/configure @@ -0,0 +1,17 @@ +#!/bin/sh +if test -z $PYTHON; then + PYTHON=python +fi + +if ! which $PYTHON > /dev/null; then + echo "'$PYTHON' not found. Try to set the environment variable PYTHON." + exit 1 +fi + + +if ! $PYTHON -c "print('testing')" > /dev/null ; then + echo "'$PYTHON' failed to execute basic test script. Try to set the environment variable PYTHON with a working Python interpreter." + exit 1 +fi + +$PYTHON scripts/mk_make.py $*