Function getPinnedInsertIndex

src/lib/editorManager.js:2235–2240

(skipFile = null)

	}

	function getPinnedInsertIndex(skipFile = null) {
		return manager.files.reduce((count, file) => {
			if (file === skipFile) return count;
			return count + (file.pinned ? 1 : 0);
		}, 0);
	}

	function syncOpenFileList() {
		const $list = manager.openFileList;