Jens Schuppe 746b4304d1 Merge branch 'dev_16' into dev_13_dev_15_dev_16		2020-01-16 10:43:51 +01:00
..
Profile.php	Merge branch 'dev_16' into dev_13_dev_15_dev_16	2020-01-16 10:43:51 +01:00
Settings.php	Fix code style issues.	2018-10-10 10:22:28 +02:00