aboutsummaryrefslogtreecommitdiff
path: root/dev/include_dune
diff options
context:
space:
mode:
authorMichael Soegtrop2021-03-23 21:52:04 +0100
committerMichael Soegtrop2021-03-23 21:52:04 +0100
commitfa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88 (patch)
tree02838cbe413809dacc416d0e71102aac9f37ae1c /dev/include_dune
parent285d5e03a230af7b327cba0b7720217ede664761 (diff)
parentaba594ca194390bb00f8ef60ef8a5eef6694fc07 (diff)
Merge PR #13914: Allow the presence of type casts for return values in Ltac2.
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions