diff configure @ 36319:4e5239ebd43d

Avoid some code duplication.
author reimar
date Fri, 09 Aug 2013 20:11:22 +0000
parents ebf1b3af62cd
children 7129dbdaae8c
line wrap: on
line diff