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.

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

Separate commands for html generation of page+units and implementation #1188

Merged
merged 12 commits into from
Aug 22, 2024

Commits on Aug 20, 2024

  1. Remove source tree

    This has never been used and is not the way to go with odoc 3
    panglesd committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    2bb99a0 View commit details
    Browse the repository at this point in the history
  2. Remove source_dir IDs

    We don't make the distinction anymore in odoc3.
    
    This also removes the --source-root argument.
    panglesd committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    d71c789 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    356fc49 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    a22f77f View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    7de9279 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    ca5b5ea View commit details
    Browse the repository at this point in the history
  7. Update man strings

    panglesd committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    c615854 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    a310ec1 View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2024

  1. Configuration menu
    Copy the full SHA
    373a144 View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2024

  1. CLI for generating source: invert source and impl order

    Source is now the positional argument, while impl is passed as an argument. When
    we generate source for other files (such as dune or .mli or Makefiles or ...)
    this will come handy.
    panglesd committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    acd14fc View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    a63b3d6 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    51fcd2d View commit details
    Browse the repository at this point in the history