[DEV-4086] add script, workflow logic and gitignore#204
Open
MarBert wants to merge 7 commits into
Open
Conversation
Contributor
There was a problem hiding this comment.
Pull request overview
Adds an on-demand workflow that synchronizes a configurable set of docs/ paths from this private repository to a public repository, backed by a new Bash sync script and a .gitignore to keep IDE files out of the repo.
Changes:
- New
workflow_dispatchworkflow with inputs for source/target branch, public repo, commit message, and comma-separated add/remove path lists; checks out both repos and commits only the files reported as modified by the sync script. - New
scripts/synch_repo.shthat validates paths against traversal patterns, normalizes adocs/prefix, copies files fromprivate_repotopublic_repo(or deletes them) and exposes amodified_filesmultiline output for the workflow. - New
.gitignoreignoring.idea/*.
Reviewed changes
Copilot reviewed 2 out of 3 changed files in this pull request and generated 11 comments.
| File | Description |
|---|---|
.github/workflows/push_on_public_repo.yml |
Defines inputs, performs the two checkouts, runs the sync script, and stages/commits/pushes the changes to the public repo. |
scripts/synch_repo.sh |
Implements path validation, copy/delete logic between private_repo and public_repo, and writes the modified-files list to GITHUB_OUTPUT. |
.gitignore |
Ignores JetBrains IDE settings. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| PATHS_TO_REMOVE: ${{ inputs.paths_to_remove }} | ||
| run: | | ||
| chmod +x scripts/synch_repo.sh | ||
| ./scripts/synch_repo.sh |
Comment on lines
+42
to
+48
| uses: actions/checkout@v4 | ||
| with: | ||
| ref: ${{ inputs.base_branch }} | ||
| path: private_repo | ||
|
|
||
| - name: Checkout public repository | ||
| uses: actions/checkout@v4 |
Comment on lines
+11
to
+13
| MODIFIED_FILES_LIST="MODIFIED_FILES_LIST.txt" | ||
| : > "$MODIFIED_FILES_LIST" # Empty or create the file on startup | ||
|
|
Comment on lines
+87
to
+90
| validate_path "$path" | ||
| if [[ "$path" != docs/* ]]; then | ||
| path="docs/$path" | ||
| fi |
Comment on lines
+65
to
+75
| find "$path" -type f | while read -r file; do | ||
|
|
||
| # Create the destination folder structure in public_repo | ||
| mkdir -p "../public_repo/$(dirname "$file")" | ||
|
|
||
| # Copy the single file | ||
| cp "$file" "../public_repo/$file" | ||
|
|
||
| # Register the file in the list (saving the relative path) | ||
| echo "$file" >> "../$MODIFIED_FILES_LIST" | ||
| done |
Sebastiano-Bertolin
requested changes
May 28, 2026
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> Co-authored-by: Sebastiano Bertolin <56671015+Sebastiano-Bertolin@users.noreply.github.com>
marcobottaro
requested changes
May 28, 2026
| required: true | ||
| default: 'main' | ||
| type: string | ||
| public_repository: |
Collaborator
There was a problem hiding this comment.
Maybe you should consider replacing "public" with "target" everywhere
| public_repository: | ||
| description: 'Name of the public repository to push to (owner/repo format)' | ||
| required: true | ||
| default: 'pagopa/public_doc' |
Collaborator
There was a problem hiding this comment.
Suggested change
| default: 'pagopa/public_doc' | |
| default: 'pagopa/developer-portal-docs' |
Comment on lines
+69
to
+70
| GH_USER: ${{ vars.GH_USER_NAME }} | ||
| GH_MAIL: ${{ vars.GH_MAIL }} |
Collaborator
There was a problem hiding this comment.
Suggested change
| GH_USER: ${{ vars.GH_USER_NAME }} | |
| GH_MAIL: ${{ vars.GH_MAIL }} | |
| GH_USER_NAME: ${{ vars.GH_USER_NAME }} | |
| GH_USER_EMAIL: ${{ vars.GH_USER_EMAIL }} |
| cd public_repo | ||
|
|
||
| # Read from the safe environment variables | ||
| git config user.name "$GH_USER" |
Collaborator
There was a problem hiding this comment.
Suggested change
| git config user.name "$GH_USER" | |
| git config user.name "$GH_USER_NAME" |
|
|
||
| # Read from the safe environment variables | ||
| git config user.name "$GH_USER" | ||
| git config user.email "$GH_MAIL" |
Collaborator
There was a problem hiding this comment.
Suggested change
| git config user.email "$GH_MAIL" | |
| git config user.email "$GH_USER_EMAIL" |
| # Safely commit and push using environment variables | ||
| git commit -m "$COMMIT_MESSAGE" | ||
| git push origin "$TARGET_BRANCH" | ||
| fi No newline at end of file |
Collaborator
There was a problem hiding this comment.
Suggested change
| fi | |
| fi | |
Comment on lines
+42
to
+52
| # Handle 'docs' prefix safely | ||
| if [[ "$path" == "docs" || "$path" == "docs/" ]]; then | ||
| path="docs" | ||
| elif [[ "$path" != docs/* ]]; then | ||
| path="docs/$path" | ||
| fi | ||
|
|
||
| echo "-> Handling path: $path" | ||
|
|
||
| # 1. Search inside public_repo; if found, delete recursively | ||
| if [[ -e "public_repo/$path" ]]; then |
Collaborator
There was a problem hiding this comment.
The public documentation should not be placed inside the docs folder. You should consire removing it from the paths in input
This file contains hidden or 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
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.
This pull request introduces a new workflow and supporting script to automate pushing documentation from a private repository to a public one, with flexible options for selecting branches, commit messages, and which documentation paths to add or remove. The main changes include the addition of workflow inputs for customization, a secure and robust Bash script for syncing files, and improved handling of file operations to ensure safety and traceability.
Workflow enhancements and automation:
.github/workflows/push_on_public_repo.yml) that allows users to specify the source and target branches, public repository, commit message, and comma-separated lists of documentation paths to add or remove. These inputs make the workflow highly configurable for different documentation update scenarios.Secure and robust synchronization script:
scripts/synch_repo.sh, a Bash script that securely processes the specified paths to add or remove, validates input paths to prevent security issues (such as directory traversal), and performs the necessary file operations between the private and public repositories.