Remove non ASCII characters

The most non ASCII characters were used in comments but some were also used
for screen output. The most common non ASCII character was µ which was
exchanged by mu or micro.