diff options
| author | Emilio Jesus Gallego Arias | 2017-03-08 14:26:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-07 02:56:18 +0200 |
| commit | 633e40b6f925556e94347c348a2804cdc1068d88 (patch) | |
| tree | b8063831a6a2ca60cf45d903dedf11f83b308fe5 /dev | |
| parent | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (diff) | |
[camlpX] Enrico's changes to camlp4 removal.
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions