aboutsummaryrefslogtreecommitdiff
path: root/ci
diff options
context:
space:
mode:
authorPierre Courtieu2020-05-04 14:40:59 +0200
committerPierre Courtieu2020-05-04 14:40:59 +0200
commit23db83dc4141d89530f6381ba49f56399682d4e0 (patch)
treedf0525f36f3a03863ea688c88bbfcd04c20030a8 /ci
parent84b81a84db632a97cc978494f2a5609525034223 (diff)
Fixing #485, bug on proof without "Proof".
Due to a re-search that should fail silently.
Diffstat (limited to 'ci')
0 files changed, 0 insertions, 0 deletions