fix mgit rng initialization, add mgit mtime command #9

Merged

reynir merged 2 commits from mgit-mtime into main

2024-12-19 13:30:01 +00:00

reynir commented

2024-12-18 14:40:58 +00:00

Owner

This first of all fixes the RNG initialization in app/mgit so it is usable with a remote.

Then second of all it adds a new repl command mtime which displays the last_modified for a given file.

This shows there is a bug in last_modified:

$ dune exec -- app/mgit.exe https://git.robur.coop/reynir/blog.robur.coop.git
# mtime index.html                 
2024-12-18 14:34:13 +00:00
# mtime index.html
2024-12-18 14:34:35 +00:00

The expected time stamp is 2024-10-28 12:10:14 +00:00 in both cases.

This first of all fixes the RNG initialization in app/mgit so it is usable with a remote. Then second of all it adds a new repl command `mtime` which displays the last_modified for a given file. This shows there is a bug in `last_modified`: ``` $ dune exec -- app/mgit.exe https://git.robur.coop/reynir/blog.robur.coop.git # mtime index.html 2024-12-18 14:34:13 +00:00 # mtime index.html 2024-12-18 14:34:35 +00:00 ``` The expected time stamp is `2024-10-28 12:10:14 +00:00` in both cases.

reynir added 2 commits 2024-12-18 14:40:59 +00:00