Integrated: Fix formatting in sample/time

Tue Sep 20 12:26:05 UTC 2022

On Tue, 20 Sep 2022 11:07:25 GMT, Per Minborg <duke at openjdk.org> wrote:

> This PR formats the time so that single-digit minutes will look better.

This pull request has now been integrated.

Changeset: 4938c40d
Author:    Per Minborg <pminborg at gmail.com>
Committer: Athijegannathan Sundararajan <sundar at openjdk.org>
URL:       https://git.openjdk.org/jextract/commit/4938c40d71e6d7cae1818d2c88a8c8ce2b247109
Stats:     1 line in 1 file changed: 0 ins; 0 del; 1 mod

Fix formatting in sample/time

-------------

PR: https://git.openjdk.org/jextract/pull/73