log_checkpoints, microseconds

The following code appears within md.c:

if (seg != NULL &&
    FileSync(seg->mdfd_vfd) >= 0)
{
    /* Success; update statistics about sync timing */
    INSTR_TIME_SET_CURRENT(sync_end);
    sync_diff = sync_end;
    INSTR_TIME_SUBTRACT(sync_diff, sync_start);
    elapsed = INSTR_TIME_GET_MICROSEC(sync_diff);
    if (elapsed > longest)
        longest = elapsed;
    total_elapsed += elapsed;
    processed++;
    if (log_checkpoints)
        elog(DEBUG1, "checkpoint sync: number=%d file=%s time=%.3f msec",
             processed,
             FilePathName(seg->mdfd_vfd),
             (double) elapsed / 1000);

    break;    /* out of retry loop */
}

Did the author of this code really intend that "elapsed" microseconds
be divided by 1000 like this?
--
Peter Geoghegan