public HeightRecord(final Label label, final int height) {
			if (ClassEditor.DEBUG || CodeArray.DEBUG) {
				System.out.println("    push " + label + " at " + height);
			}

			this.label = label;
			this.height = height;
		}