Skip to content

add link to tutorial-symbolics on main page#73

Merged
ocots merged 1 commit into
mainfrom
update-symbolics
May 11, 2026
Merged

add link to tutorial-symbolics on main page#73
ocots merged 1 commit into
mainfrom
update-symbolics

Conversation

@abavoil
Copy link
Copy Markdown
Collaborator

@abavoil abavoil commented May 10, 2026

prêt à merge (je m'étais arrêté en plan sur la dernière PR)

@github-actions github-actions Bot requested a review from ocots May 10, 2026 18:12
@ocots ocots added the run documentation Trigger Documentation label May 10, 2026
@ocots
Copy link
Copy Markdown
Member

ocots commented May 10, 2026

on laisse tourner la documentation et on voit.

@abavoil
Copy link
Copy Markdown
Collaborator Author

abavoil commented May 10, 2026

Si tout est bon tu peux supprimer les branches symbolics-update et update-symbolics 😉

@ocots ocots merged commit 2b3baec into main May 11, 2026
7 checks passed
@ocots ocots deleted the update-symbolics branch May 11, 2026 07:08
@ocots
Copy link
Copy Markdown
Member

ocots commented May 11, 2026

De ton côté en local, tu peux faire un git remote prune origin et git branch -d branch-name pour nettoyer.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

run documentation Trigger Documentation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants