diff mx/eclipse-settings/org.eclipse.jdt.ui.prefs @ 5132:e1a03c81cef0

another fix for non-graal builds
author Lukas Stadler <lukas.stadler@jku.at>
date Wed, 21 Mar 2012 13:05:57 +0100
parents 04ebcabcba4f
children 44d92b447951
line wrap: on
line diff