Closed giordano closed 5 months ago
Fix #322.
As an evidence that this worked: the job triggered by the merged of this PR didn't do anything and exited successfully.
Fix #322.