diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/configure b/configure index 6207a85e..644ee3e9 100755 --- a/configure +++ b/configure @@ -1784,8 +1784,6 @@ fi ac_config_files="$ac_config_files Makefile.config" -ac_config_files="$ac_config_files stp/Makefile.common" - ac_config_headers="$ac_config_headers include/klee/Config/config.h" |