configure
branchnoai
changeset 9621 7654501cf02d
parent 9566 9936b201d53f
child 9626 79f2b5a0cdd7
--- a/configure	Wed May 09 20:22:49 2007 +0000
+++ b/configure	Thu May 10 15:07:16 2007 +0000
@@ -95,6 +95,7 @@
 		if ($0 == "MSVC"        && "'$os'" != "MSVC")              { next; }
 		if ($0 == "DIRECTMUSIC" && "'$with_direct_music'" == "0")  { next; }
 		if ($0 == "LIBTIMIDITY" && "'$libtimidity'" == "" )        { next; }
+		if ($0 == "NO_THREADS"  && "'$with_threads'" == "0")       { next; }
 
 		skip += 1;