# HG changeset patch
# User etisserant
# Date 1178901294 -7200
# Node ID 3248a2d6bb0bcdd21de5795e38de45e90c786ef4
# Parent  1c1d1893f1c9fbfba815a5814e2df5319c6b055b
Let user choose his own XENO_CONFIG.

diff -r 1c1d1893f1c9 -r 3248a2d6bb0b configure
--- a/configure	Fri May 11 18:34:26 2007 +0200
+++ b/configure	Fri May 11 18:34:54 2007 +0200
@@ -79,7 +79,9 @@
 test=conftest
 rm -f $test $test.c
 
-XENO_CONFIG=/usr/xenomai/bin/xeno-config
+if [ "$XENO_CONFIG" == "" ]; then
+	XENO_CONFIG=/usr/xenomai/bin/xeno-config
+fi
 
 ###########################################################################
 #                          ARGUMENTS PARSING                              #