[ros-diffs] [gvg] 12892: makefile.dos is not used anymore, remove to prevent confusion