diff options
| author | Erik Martin-Dorel | 2019-12-09 21:31:10 +0100 |
|---|---|---|
| committer | GitHub | 2019-12-09 21:31:10 +0100 |
| commit | cf904b955056f16e46d1541b3ffb1ca1533c936d (patch) | |
| tree | 5693436fb30135fccf170cf7b15991b5c5dee0fd /generic | |
| parent | b893f682a9bbd0f42dfd4501dc0451ab1e4ec713 (diff) | |
| parent | 986fefde8e2f5b942f9715b4e423c6a350497004 (diff) | |
Merge pull request #447 from ProofGeneral/fix-gh-446
Recognize "Timeout" before save keywords to fix #446
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions