diff options
| author | Théophane Hufschmitt <7226587+thufschmitt@users.noreply.github.com> | 2022-12-09 06:33:30 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-12-09 06:33:30 +0100 |
| commit | 2affb19c921c3c5c3f7628a65dbcdb74f36f5222 (patch) | |
| tree | 595cd6799a16398364b0bfa20c6c1316f2327b8b /Makefile.config.in | |
| parent | 1dd7779c7cdca7061e80ebc3b7886a2aa97b0d8a (diff) | |
| parent | 1c8de7d3d03d7a6ba259387b0698874fa879428c (diff) | |
Merge pull request #7409 from tweag/fix-6383
check the store for input before failing (hopefully fix #6383)
Diffstat (limited to 'Makefile.config.in')
0 files changed, 0 insertions, 0 deletions