aboutsummaryrefslogtreecommitdiff
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-05-19 14:12:30 +0200
committerGaëtan Gilbert2020-05-19 14:12:30 +0200
commit407ca661d7eb33afed706afe74f11fccac2f1dd4 (patch)
treed867bc7f77bfeb1c9a09598f7945d7d77f1ccae3 /Makefile.doc
parent2222e455f0501b700f198ab614d8743229062f73 (diff)
parent833d7672a4cc1dbdd4ab5a861362824b03f72d57 (diff)
Merge PR #12301: [declare] Grand unification of the proof save path.
Reviewed-by: SkySkimmer Ack-by: ppedrot
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions