aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorMichael Soegtrop2020-12-27 11:50:11 +0100
committerMichael Soegtrop2020-12-27 11:51:01 +0100
commitced34256415b7c37c3eca11cb01fa7eb91cc518d (patch)
tree22aca442be7f625538329060eb1285b648b69afe /plugins
parent61089d86149c87de3078a5217593a9d0aef5e402 (diff)
CoqIDE: Fix CC reference in makefile
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions