diff --git a/configure b/configure index deb62aff003b520ac9580fb78e14e614d5c0955e..3c5fb6ecc749940509305d1e18b3d12bf9664509 100755 --- a/configure +++ b/configure @@ -1797,9 +1797,8 @@ else exit 1 fi -if test "$xen" = "yes" ; - then - echo "CONFIG_XEN=y" >> $config_host_mak +if test "$xen" = "yes" ; then + echo "CONFIG_XEN=y" >> $config_host_mak fi tools=