aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-03-19 15:46:13 +0100
committerPierre-Marie Pédrot2019-03-19 15:46:13 +0100
commit2b68b2223527b5bc247bd338ae4613a00654636c (patch)
tree940db9f99a47fa996c1374446f6d944ca5183d21 /plugins/syntax
parentf1ca51445650a6595a9dfd28c365b83fa25d1eea (diff)
parentcef009d27d79b90ee42e0ea96c487d5a07d803de (diff)
Merge PR #9279: CoqIDE on lablgtk3
Ack-by: MSoegtropIMC Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: garrigue Ack-by: herbelin
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions