aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEnrico Tassi2019-02-20 13:24:34 +0100
committerEnrico Tassi2019-02-20 13:24:34 +0100
commit756b978dfee0e0c103a5244af21115233ad96358 (patch)
tree937b01faf9e2aba41c1396f544d5d2a9ab3ec426 /dev
parentc39482e63aacf47359d8f76c44c2d851c7cfb9a5 (diff)
parent49ed4b7d3a01b9c383bb99fc26a7b34a7a711fdf (diff)
Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlib
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions