Pekka Enberg d75817998d Add merge-pr.py helper script ...

This adds a helper script to generate merge commits that are nicer than
the default Github one.

2024-08-01 10:23:06 +03:00

..

merge-pr.py

Add merge-pr.py helper script

2024-08-01 10:23:06 +03:00