Skip to content

Conversation

@romintomasetti
Copy link
Contributor

This PR adds:

  • the package
  • some CI
  • a devcontainer

@romintomasetti romintomasetti self-assigned this Sep 28, 2024
@romintomasetti romintomasetti force-pushed the first branch 20 times, most recently from e565cf8 to 5fe9997 Compare September 28, 2024 04:06
@maartenarnst
Copy link
Contributor

maartenarnst commented Sep 29, 2024

OK. I've taken a look at the PR. It all looks good. From the bigger picture point of view, there's the question of whether we want to extract from the tools in trilinos-container separate pieces like we do here for the apt helpers. Or whether we'd want to extract the entire tools. It's a bit the question of how all the helpers would be most readable to the "outside" world: several small repos vs one larger repo. Thinking about it the other way around, we could also think whether it may make sense to suggest these helpers as features in an issue on the apt GitHub. Keeping it as is here would be OK for me, but probably best discussed a bit live.

@romintomasetti romintomasetti force-pushed the first branch 5 times, most recently from de4ccc8 to 0c3c310 Compare September 30, 2024 14:13
@maartenarnst
Copy link
Contributor

OK. I've just read through the entire PR once more. It's very nice! Just a few details left.

@romintomasetti romintomasetti force-pushed the first branch 2 times, most recently from 8f1a3b1 to 3ddc4e2 Compare October 7, 2024 13:21
Copy link
Contributor

@maartenarnst maartenarnst left a comment

Choose a reason for hiding this comment

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

OK! 🟢

Copy link
Contributor

@maartenarnst maartenarnst left a comment

Choose a reason for hiding this comment

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

OK! Still good :) Just the thought about the "context" in the devcontainer.json.

@maartenarnst
Copy link
Contributor

I’ll let you merge.

@romintomasetti romintomasetti merged commit 4aacdc8 into main Oct 7, 2024
3 checks passed
@romintomasetti romintomasetti deleted the first branch October 7, 2024 17:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants