dot product vs star symbol ?

[Helge Gabert]

Some people (myself included) prefer the star for the multiplication symbol. Dots are too similar to decimal points, and can be confusing to the eye.

But it would be OK to make that available as a setup option, so the user can choose.