diff options
| author | Gaëtan Gilbert | 2020-12-11 12:17:44 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-12-11 12:17:44 +0100 |
| commit | b98d4349907ccbb01d5fe5ea69d7923c6a6d3c63 (patch) | |
| tree | 744c7a127a4bf903acaa66b5164f386370e244c0 /pretyping | |
| parent | 1918f19cb43d6d4313276b167af38316b27879f2 (diff) | |
Bench: add .log extension to .stdout/stderr files
Hopefully this allows viewing online with a download dialog on gitlab.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions