# This is used to avoid adding an extern file more than once
	private var seen_extern = new ArraySet[String]