Commit 53806e5b83cee0e275eac038d0780f95ac56588c

Behdad Esfahbod 2020-11-25T11:51:37

Tiny improvement on previous commit Functionally the same.