configure
changeset 6004 03795fd01cb8
parent 5840 a1dba7cd499c
child 6192 c6adfc929c6b
--- a/configure	Sun Jan 21 13:16:31 2007 +0000
+++ b/configure	Sun Jan 21 14:14:27 2007 +0000
@@ -38,7 +38,7 @@
 make_cflags_and_ldflags
 
 EXE=""
-if [ "$os" = "MINGW" ] || [ "$os" = "CYGWIN" ] || [ "$os" = "OS2" ]; then
+if [ "$os" = "MINGW" ] || [ "$os" = "CYGWIN" ] || [ "$os" = "OS2" ] || [ "$os" = "WINCE" ]; then
 	EXE=".exe"
 fi
 
@@ -78,6 +78,7 @@
 		if ($0 == "BEOS"        && "'$os'" != "BEOS")              { next; }
 		if ($0 == "WIN32"       && "'$os'" != "MINGW" &&
 		                "'$os'" != "CYGWIN" && "'$os'" != "MSVC" ) { next; }
+		if ($0 == "WINCE"       && "'$os'" != "WINCE")             { next; }
 		if ($0 == "MSVC"        && "'$os'" != "MSVC")              { next; }
 		if ($0 == "DIRECTMUSIC" && "'$with_direct_music'" == "0")  { next; }