aboutsummaryrefslogtreecommitdiff
path: root/pgshell
diff options
context:
space:
mode:
authorErik Martin-Dorel2019-12-08 01:32:28 +0100
committerErik Martin-Dorel2019-12-08 14:23:58 +0100
commit986fefde8e2f5b942f9715b4e423c6a350497004 (patch)
tree5693436fb30135fccf170cf7b15991b5c5dee0fd /pgshell
parentb893f682a9bbd0f42dfd4501dc0451ab1e4ec713 (diff)
fix: Recognize "Timeout" before save keywords
viz. '("Defined" "Save" "Qed" "End" "Admitted" "Abort" "Proof")
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions