diff options
| author | Théo Zimmermann | 2018-10-26 10:08:54 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-26 10:08:54 +0200 |
| commit | ebf38e474ad96e430f0cbeef533e2faab5748eeb (patch) | |
| tree | 71396b33c8f5b42efa13d0e488508e26aa2702b2 /interp | |
| parent | 1531b831017d594002ed21a966b62081b5e003a6 (diff) | |
[default.nix] Clean-up: use camlp5 instead of synonymous camlp5_strict.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions