aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-03 23:48:26 +0000
committerGitHub2020-11-03 23:48:26 +0000
commit5a25287987b8683ee3cbaa9a87ba0f8aebba896b (patch)
treedce1ab90cc6785e29848e43deaea6c24b4138866 /plugins
parent077d479113c6a53543d53514470be3570c89cc8d (diff)
parent87be983b7623126320dc0b43303a48ea41b86f5c (diff)
Merge PR #13293: Doc: added "Arguments" removing implicit arguments
Reviewed-by: jfehrle Reviewed-by: Zimmi48
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions