chiark / gitweb /
gremlin/gremlin.in: Update progress every 100ms rather than 200ms.
authorMark Wooding <mdw@distorted.org.uk>
Thu, 19 Apr 2018 10:52:28 +0000 (11:52 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Fri, 20 Apr 2018 12:18:27 +0000 (13:18 +0100)
commitfbbde927eeb917bc5d5076259da5d9881b3816ca
treed9814fc50683fe443697bd77c9035d88bceb33a2
parente9bf7f71307405c89e34d7e337f11ff370848cbc
gremlin/gremlin.in: Update progress every 100ms rather than 200ms.

Makes the display subjectively much smoother.
gremlin/gremlin.in