Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 12 additions & 5 deletions .github/copilot-instructions.md
Original file line number Diff line number Diff line change
Expand Up @@ -136,9 +136,9 @@ When working with public API changes:

1. **NEVER commit directly to `main`** - Always create a feature branch for your work. Direct commits to `main` are strictly prohibited.

2. **Do NOT rebase, squash, or force-push** unless explicitly requested by the user. These operations rewrite git history and can cause problems for other contributors. Default behavior should be regular commits and pushes.
2. **When amending an existing PR, work on the PR's branch directly** - Do NOT create a separate branch off a PR branch. The PR branch already IS a feature branch. Creating a new branch off it means CI won't run on the original PR, defeating the purpose. Use `gh pr checkout` to switch to the PR branch, make your changes, commit, **then** ask before pushing so the user can review locally first.

3. **When amending an existing PR, do NOT automatically push** - After making changes to an existing PR branch, ask the user before pushing. This allows the user to review the changes locally first. Exception: If the user's instructions explicitly include pushing, proceed without asking.
3. **Do NOT rebase, squash, or force-push** unless explicitly requested by the user. These operations rewrite git history and can cause problems for other contributors. Default behavior should be regular commits and pushes.

**Safe Git Workflow:**
```bash
Expand All @@ -157,9 +157,16 @@ git push
```

**When asked to update an existing PR:**
1. Make the requested changes
2. Stage and commit the changes
3. **STOP and ask the user** before pushing: "Changes are committed locally. Would you like me to push these changes to the PR?"
```bash
# Check out the PR branch directly (do NOT create a new branch off it)
gh pr checkout 12345

# Make fixes and commit to the PR branch
git add .
git commit -m "Fix: Description of the change"
```
1. **STOP and ask the user** before pushing: "Changes are committed locally. Would you like me to push these changes to the PR?"
2. Exception: If the user's instructions explicitly include pushing, proceed without asking.

### Documentation
- Update XML documentation for public APIs
Expand Down