diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -710,6 +710,7 @@ HAS_STANDARD_HEADERS=$has_standard_headers INSTALL_COQDEV=$install_coqdev LIBMATH=$libmath MODEL=$model +OS=${os:-unspecified} SYSTEM=$system RESPONSEFILE=$responsefile LIBRARY_FLOCQ=$library_Flocq |