seems to fix the problem, fairly harmlessly (*maybe* there are some
edge cases where the integer and floating-point computations give
different answers??? these values are going to get sent to qr.solve() a
few lines later in any case ...)
If people think this is worthwhile I could submit a bug report.