diff options
| author | Théo Zimmermann | 2020-05-12 11:30:25 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:39:09 +0200 |
| commit | eae7b25e06b75f1c890215d4e6176292f10f854a (patch) | |
| tree | 3071f201d0cb97f1264f975375ce79ca49d85a41 /dev/include | |
| parent | 7026c498264e32f1ffbeb7767872d00babdbd341 (diff) | |
Deprecate SearchHead.
The main use case of SearchHead is now handled by headconcl:
The secondary use case was redundant with SearchPattern.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions