Björn Schießle a7bb4b128f personal settings removed, there is no need to expire versions manually		2012-12-17 13:34:17 +01:00
..
versions.js	don't call $('#found_versions').chosen(); after opening the history drop-down since no version is selected at the beginning	2012-10-27 15:50:17 +02:00