Updated Docker image #123
Closed
Updated Docker image #123
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
podhrmic
reviewed
Sep 29, 2022
podhrmic
approved these changes
Sep 29, 2022
podhrmic
requested changes
Sep 29, 2022
|
@SimplisticCode any updates? |
added 3 commits
October 6, 2022 09:09
This reverts commit c5c0e32.
podhrmic
approved these changes
Nov 2, 2022
|
If @kiniry is OK with unsigned commits, then we can merge this once @SimplisticCode tests and uploads the new image. |
|
I'm testing this PR. Now that Ubuntu 22.10 came out, the Docker images for the 21 release are gone, so I've moved the base of this image back to 20 for testing. |
|
I have had to update the location of the RDE_RF tool from Simon's personal organization to its new home in Galois's. I'm testing builds of the image now, and after successfully building, I'll push a new release to DockerHub. |
|
@kiniry Simon didn't sign his commits - do you want to just merge as is? |
podhrmic
added a commit
that referenced
this pull request
Feb 9, 2023
|
Closing in favor of #138 |
|
We forgot to delete the branch. I'll take care of it. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Updated Docker image to fetch and put the documentation enricher in the path.
I furthermore included a shell script to run the tool easily with some default parameters.