diff configure @ 352:4905a1d9e6a7

minor improvement of output of devel/are-options-documented
author markus schnalke <meillo@marmaro.de>
date Sun, 04 Sep 2011 10:14:36 +0200
parents 3f1eecd8082d
children 92340177150d
line wrap: on
line diff