diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -113,6 +113,7 @@ AWKCOMMAND=' if ($0 == "OS2" && "'$os'" != "OS2") { next; } if ($0 == "PSP" && "'$os'" != "PSP") { next; } if ($0 == "DEDICATED" && "'$enable_dedicated'" != "1") { next; } + if ($0 == "AI" && "'$enable_ai'" == "0") { next; } if ($0 == "COCOA" && "'$with_cocoa'" == "0") { next; } if ($0 == "DOS" && "'$os'" != "DOS") { next; } if ($0 == "BEOS" && "'$os'" != "BEOS" && |