comparison mx/eclipse-settings/org.eclipse.jdt.ui.prefs @ 14123:dc41eab09fe8

gate: add non-tiered bootstrap
author Bernhard Urban <bernhard.urban@jku.at>
date Mon, 10 Mar 2014 16:20:45 +0100
parents 3417a9177425
children
comparison
equal deleted inserted replaced
14122:2a7d7da912e1 14123:dc41eab09fe8