Daniel Gultsch c19adebaf0 open files with capital extensions as well. fixes #1354		2015-08-23 21:00:51 +02:00
..
main	open files with capital extensions as well. fixes #1354	2015-08-23 21:00:51 +02:00