configure
branchcpp_gui
changeset 6254 abc6ad7c035c
parent 6208 ff9b5772fb65
child 6268 4b5241e5dd10
--- a/configure	Wed Feb 14 10:46:38 2007 +0000
+++ b/configure	Sat Feb 17 11:12:50 2007 +0000
@@ -82,6 +82,7 @@
 		if ($0 == "WINCE"       && "'$os'" != "WINCE")             { next; }
 		if ($0 == "MSVC"        && "'$os'" != "MSVC")              { next; }
 		if ($0 == "DIRECTMUSIC" && "'$with_direct_music'" == "0")  { next; }
+		if ($0 == "LIBTIMIDITY" && "'$libtimidity'" == "" )        { next; }
 
 		skip += 1;