summaryrefslogtreecommitdiff
path: root/include
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2020-02-06 17:55:15 -0500
committerGravatar GitHub <noreply@github.com>2020-02-06 17:55:15 -0500
commitb0690cc786c858b4a41c7682937bebd53d318f6a (patch)
tree24f36ba4a06ab465c185e93ac38959d663944cd0 /include
parentdbdf458dc49191a6f355a16bae839a2d618513b7 (diff)
parent5ed96ea023de0570061660363ee55c3f9cffda18 (diff)
Merge pull request #196 from mdempsky/manual-edits
Manual edits
Diffstat (limited to 'include')
0 files changed, 0 insertions, 0 deletions