Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add various terms to the glossary #281

Merged
merged 6 commits into from
Feb 18, 2019
Merged

Add various terms to the glossary #281

merged 6 commits into from
Feb 18, 2019

Commits on Feb 16, 2019

  1. Add "lang item" to glossary

    @varkor
    varkor committed Feb 16, 2019
    Configuration menu
    Copy the full SHA
    e2f8c71 View commit details
    Browse the repository at this point in the history

  2. Add "item" to glossary

    @varkor
    varkor committed Feb 16, 2019
    Configuration menu
    Copy the full SHA
    1d0e5e9 View commit details
    Browse the repository at this point in the history

  3. Add "early-bound lifetime" and "late-bound lifetime" to the glossary

    @varkor
    varkor committed Feb 16, 2019
    Configuration menu
    Copy the full SHA
    5d994ec View commit details
    Browse the repository at this point in the history

  4. Add "intern" to the glossary

    @varkor
    varkor committed Feb 16, 2019
    Configuration menu
    Copy the full SHA
    bbdd85e View commit details
    Browse the repository at this point in the history

  5. Add "memoise" to the glossary

    @varkor
    varkor committed Feb 16, 2019
    Configuration menu
    Copy the full SHA
    b2aa4c1 View commit details
    Browse the repository at this point in the history

  6. Add "drop glue" to the glossary

    @varkor
    varkor committed Feb 16, 2019
    Configuration menu
    Copy the full SHA
    9a67be4 View commit details
    Browse the repository at this point in the history