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

User-defined mapping: add option for multiple mapping files #289

Closed
Tracked by #256
mknorps opened this issue Apr 3, 2023 · 0 comments · Fixed by #306
Closed
Tracked by #256

User-defined mapping: add option for multiple mapping files #289

mknorps opened this issue Apr 3, 2023 · 0 comments · Fixed by #306
Assignees
@mknorps
Labels
P2 major: an upcoming release
Milestone
Mapping strategy

Comments

@mknorps
Copy link
Collaborator

mknorps commented Apr 3, 2023

No description provided.

@mknorps mknorps added this to the Mapping strategy milestone Apr 3, 2023
@mknorps mknorps added the P2 major: an upcoming release label Apr 3, 2023
This was referenced Apr 3, 2023
Merged
Closed
@mknorps mknorps self-assigned this Apr 13, 2023
@mknorps mknorps linked a pull request Apr 14, 2023 that will close this issue
User defined mapping: add option and handling for multiple mapping files #306
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mknorps mknorps

Labels
P2 major: an upcoming release
Projects
None yet
Milestone
Mapping strategy
Development

Successfully merging a pull request may close this issue.

User defined mapping: add option and handling for multiple mapping files tweag/FawltyDeps
1 participant
@mknorps