diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -994,6 +994,7 @@ let coqideincl = "$LABLGTKINCLUDES" let cflags = "$cflags" let best = "$best_compiler" let arch = "$ARCH" +let has_coqide = "$COQIDE" let has_natdynlink = $HASNATDYNLINK let natdynlinkflag = "$NATDYNLINKFLAG" let osdeplibs = "$OSDEPLIBS" |