diff options
| author | Erik Martin-Dorel | 2020-04-21 22:02:58 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-21 22:02:58 +0200 |
| commit | b53f58e96c1cc2c8d401dd382624f572e3458284 (patch) | |
| tree | 99761d83ac68c18988777a59cadbbe229b5fed7f /pgshell/example.pgsh | |
| parent | 18311b7cc64bbe2b271a45d72b4ba2affa5213bd (diff) | |
| parent | 2346bbafa9dcefe5ed344e758c399e1507817b43 (diff) | |
Merge pull request #483 from ProofGeneral/use-github-actions
Use GitHub actions
Diffstat (limited to 'pgshell/example.pgsh')
0 files changed, 0 insertions, 0 deletions