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

config: allow config filename per repo #151

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

Khady
Copy link
Contributor

@Khady Khady commented Jun 2, 2024

Currently the config filename is set globally for all the repository. It's not really convenient because it doesn't allow any exception, and if one wants to change the filename it has to be done for all the repositories.

The existing code is a bit disorganised too. For example the default config name exists in two places with different values:

Arg.(value & opt string ".monorobot.json" & info [ "config" ] ~docv:"CONFIG" ~doc)

let default_config_filename = "monorobot.json"

This PR adds yet another place where this can be set. In the repo config which lives in the secrets. It's not really a secret but I didn't want to introduce an extra file for this feature.

I also thought about supporting a list of names instead of a single one. But it triggers even more changes, especially in places where there are queries done to the github api. So I decided against it for now at least.

Comment on lines +38 to +39
match get_secrets_exn ctx with
| exception Context_error _ -> ctx.config_filename
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that it would be better without this catch, but the tests are failing if I omit it.

@rr0gi
Copy link
Contributor

rr0gi commented Jun 27, 2024

i think we don't need this configurable at all, just pick some name, .monorobot.json sounds good?

@rr0gi
Copy link
Contributor

rr0gi commented Jun 27, 2024

oh i see, the request is to have it without the dot
then without dot

@Khady Khady added the Blocked label Sep 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants