diff options
| author | Pierre-Marie Pédrot | 2015-05-05 12:28:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-05 12:50:33 +0200 |
| commit | e4ca462b7d51f25b258263345835025c1c4325bd (patch) | |
| tree | 859c00670b3094406ae7acf58f48b5bffdbc26e9 /kernel/nativecode.ml | |
| parent | 6ebd2316e5acf10e0d505804fdd7001edc5575fa (diff) | |
Removing dead code in Rewrite.
The hypinfo cache was actually always set to None, so that there was no need
to try to preserve it if it was set to an actual value.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions