configure
changeset 10385 4f9838649c7f
parent 10379 dd9d0aade65e
child 10400 03e9c6b00a00
--- a/configure	Wed Nov 26 01:07:49 2008 +0000
+++ b/configure	Wed Nov 26 13:12:45 2008 +0000
@@ -50,7 +50,7 @@
 make_cflags_and_ldflags
 
 EXE=""
-if [ "$os" = "MINGW" ] || [ "$os" = "CYGWIN" ] || [ "$os" = "OS2" ] || [ "$os" = "WINCE" ]; then
+if [ "$os" = "MINGW" ] || [ "$os" = "CYGWIN" ] || [ "$os" = "OS2" ] || [ "$os" = "DOS" ] || [ "$os" = "WINCE" ]; then
 	EXE=".exe"
 fi