DropMarks in refine.cc disabled on purpose?
27 years ago Stefan Lang disabled DropMarks
with 82e4d9f7. The resulting code is misleading, as the return statement is easily overlooked.
We should investigate, if this commit was on purpose or only a temporary fixup. If it is okay, we should get rid of DropMarks
altogether.