aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/Extraction.v
AgeCommit message (Collapse)Author
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.