-
Georges Racinet authored
The Git typical messages are mostly a distraction for our users, since the push to the auxiliary Git repo is an implementation detail and they can't do anything about it anyway.
6dbe7d60e669
The Git typical messages are mostly a distraction for our users, since the push to the auxiliary Git repo is an implementation detail and they can't do anything about it anyway.