GitHub · Where software is built

Labels Milestones New issue

Add option to `extract_examples` to allow changing the directory the files are placed in.

#273

· fingolfin opened

on Dec 20, 2023

Integrate publishing of docs to GitHub Wikis

#269

· ZachNewbery opened

on Dec 5, 2022

Document better how labels are auto-assigned to declarations

#255

· fingolfin opened

on Jul 12, 2021

Add an option to turn off automatic assignment of labels to filters and categories (and maybe more)

#254

· fingolfin opened

on Jul 12, 2021

Change all generated files to have name starting with underscore

#237

· fingolfin opened

on Mar 5, 2020

Improve extract_examples to allow naming files based on the chapter or section number

#233

· fingolfin opened

on Oct 29, 2019

Add test for `extract_examples` which uses different units than the default (e.g. sections not chapter)

good first issue

#232

· fingolfin opened

on Oct 29, 2019

Explicitly define how indentation is handled, and implement this

#231

· fingolfin opened

on Sep 4, 2019

Allow setting raw chapter/section/subsection labels

#223

· fingolfin opened

on Jul 2, 2019

Merge @ChapterLabel, @SectionLabel, @SubsectionLabel into @Label ?

#222

· fingolfin opened

on Jul 2, 2019

Improve single backticks to distinguish code, arguments, keywords

#207

· fingolfin opened

on Mar 29, 2019

Add examples for using `<Ref` to the manual (in the tutorial, and ideally also after ChapterLabel, SectonLabel etc.

#185

· fingolfin opened

on Sep 20, 2018