aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-07-23 00:40:51 +0200
committerEmilio Jesus Gallego Arias2019-07-23 00:40:51 +0200
commitae82afbaebb7f3a328498d4cc541d299423a7637 (patch)
tree57f6b25e70e38ef7e92dce6fa4025e1466910744 /plugins
parent7cdab2e35f21c5bbd4f98fcb49c7b7bd24419849 (diff)
parent9b929e16b1123674c737c1cef2002f5a3c3f2d39 (diff)
Merge PR #10541: Dune: fix build_all_stdlib rule
Ack-by: ejgallego
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions