aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-04-03 11:10:08 -0400
committerEmilio Jesus Gallego Arias2020-04-03 11:10:08 -0400
commite16a279b2afe1824ccb8bf4bbc17f797ee5baf6c (patch)
treeb80b24b87cafe88ccb5aa8c7ad02a084e99becea /library
parent8a3255bc99691c7c0f9b386e63b7947169f902b7 (diff)
parent470f5e063535f91ce0e95798d4aaadfefffb89e0 (diff)
Merge PR #11664: Encoding string list as a string with application to the parsing of coqtop arguments in coqide
Reviewed-by: ejgallego
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions