Andy Williams 7455ec0f08 [editor] Make whitespace trimming an option ... Add a global setting to turn off the behaviour		2015-08-29 14:46:18 +01:00
legacy/elm_code	[editor] Make whitespace trimming an option	2015-08-29 14:46:18 +01:00