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

various changes #30

Merged
merged 5 commits into from
Jul 20, 2024
Merged

various changes #30

merged 5 commits into from
Jul 20, 2024

Conversation

iacore
Copy link
Contributor

@iacore iacore commented Dec 8, 2022 •
edited
Loading

see commits

@iacore iacore changed the title Fix 2 various changes Dec 8, 2022
@iacore
Copy link
Contributor Author

iacore commented Dec 8, 2022 •
edited
Loading

The usage text formatting is bad.

$ katla
...
  html      HTML backend
            Usage: html build/ttc/20000101/Katla.ttc
            build/ttc/20000101/Katla.ttm > out.html
    init      Generate default configuration file

    --config  Preamble configuration file in Dhall format.
              Use `init` to generate the defaults config file.

gallais
gallais reviewed Jan 17, 2023
View reviewed changes
src/Katla/CLI.idr Outdated Show resolved Hide resolved
@ohad @gallais
Update src/Katla/CLI.idr
aadd1d7 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
@ohad ohad merged commit 1db94bd into idris-community:main Jul 20, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@gallais gallais gallais left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@iacore @gallais @ohad