aboutsummaryrefslogtreecommitdiff
path: root/dev/include_printers
diff options
context:
space:
mode:
authorEnrico Tassi2020-04-06 09:53:41 +0200
committerEnrico Tassi2020-05-07 14:02:53 +0200
commit9c111b3ed2dd16b86cc8e187b5e35ebdd482668f (patch)
tree10b9e1c2d4335c29fe7138cec922f0c97ba7a775 /dev/include_printers
parent18a78b53f6998d3af8f8bb1b7a6b5054af232d4e (diff)
[win] Coq trunk is now called master
The old script was still working but downloading an old version, probably there is a git ref called trunk somewhere
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions