diff options
| author | Guillaume Melquiond | 2014-10-24 18:36:19 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-10-24 18:37:59 +0200 |
| commit | 604621edc81f1c439af5c36ee31c6977c6c3f9f0 (patch) | |
| tree | 515778a800d034723c2431a3c0c6ad3bbe100853 /kernel/type_errors.mli | |
| parent | 884b6cc6c12bd557085cdaa4972d593684c9cc1a (diff) | |
Fix generation of the index_urls.txt file.
Hevea has stopped producing HTML4 code two years ago. So the old sed
expression was producing an empty index file for any user with a
non-deprecated version of hevea.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions