Skip to content

move reinstall script to local_dev#2129

Merged
LeiGlobus merged 1 commit into
mainfrom
lei/move-reinstall-script
Jun 29, 2026
Merged

move reinstall script to local_dev#2129
LeiGlobus merged 1 commit into
mainfrom
lei/move-reinstall-script

Conversation

@LeiGlobus

Copy link
Copy Markdown
Contributor

As was suggested, move reinstall.sh to local_dev and make it runnable from any directory

@LeiGlobus LeiGlobus added the no-news-is-good-news This change does not require a news file label May 19, 2026
Comment thread local_dev/reinstall.sh Outdated
khk-globus
khk-globus previously approved these changes May 19, 2026

@khk-globus khk-globus left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Since this script is only "used by us," these aren't blockers. Your choice whether to address them.

khk-globus
khk-globus previously approved these changes Jun 29, 2026

@khk-globus khk-globus left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Observed in Slack that $SDK and $EP could also be quoted. But again, as a "only used by us" script, this is ready to go in.

@LeiGlobus LeiGlobus merged commit d8c2b46 into main Jun 29, 2026
12 checks passed
@LeiGlobus LeiGlobus deleted the lei/move-reinstall-script branch June 29, 2026 19:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

no-news-is-good-news This change does not require a news file

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants