Fix incorrect error message
- Apr 02, 2020
-
-
William Keaton Balunas authored9f4012e8
-
William Keaton Balunas authoredbe09875b
-
This is a trivial change which fixes an error message which had a mistake in it (it was writing out the wrong tool name). An obsolete and no-longer-correct comment is also removed.