log devel/are-options-documented @ 434:f2a7271746d1 default tip

age author description
2011-09-04 markus schnalke minor improvement of output of devel/are-options-documented
2010-07-23 meillo renamed misc/ to devel/ base misc/are-options-documented@b980139ed685