Code Triplecheck / Code / Diff of /tool/run/extensions/config/inf.java

Diff of /tool/run/extensions/config/inf.java [r17] .. [r18]

	a/tool/run/extensions/config/inf.java		b/tool/run/extensions/config/inf.java