Commit Graph

3 Commits

Author SHA1 Message Date
Eliaz Bobadilla b8e5068400 tools: update checkout action on CI
https://github.com/actions/checkout\#whats-new
2022-03-30 12:09:45 -05:00
Michael Howell 715bc47154 Do not include headers in search index
This significantly shrinks the pre-compressed search index:

    $ du -h searchindex-old.js searchindex-new.js
    26M	searchindex-old.js
    19M	searchindex-new.js

And shrinks the search index even after it's gzipped:

    $ du -h searchindex-old.js.gz searchindex-new.js.gz
    4.5M	searchindex-old.js.gz
    3.3M	searchindex-new.js.gz

This change requires a newer version of mdBook, with
https://github.com/rust-lang/mdBook/pull/1637
2021-10-04 09:13:37 -07:00
Eric Huss 21029cd587 Switch from travis to github actions. 2021-06-17 15:02:23 -07:00