commit test from my laptop (made useless change) · mseri/BET@a1a2abd · GitHub

Commit

commit test from my laptop (made useless change)

Browse files

Loading branch information

marcolenci committed Feb 29, 2024

1 parent 554736f commit a1a2abd

BET/Birkhoff.lean

Original file line number	Diff line number	Diff line change
Expand Up		@@ -80,5 +80,4 @@ the integral. -/

		/- Birkhoff theorem for ergodic maps. -/


		end Ergodic_Theory

4 comments on commit `a1a2abd`

Collaborator Author

marcolenci commented on `a1a2abd` Feb 29, 2024 •

edited

Loading

I've made this (innocuous) commit to test a pull request from my laptop, but I forget how to actually do the PR (both from VSC and from a shell)....

Collaborator Author

marcolenci commented on `a1a2abd` Feb 29, 2024

I suppose I had to make the change in another local branch to push it to mseri's repo or something like that (like you made me do this morning) but I did directly from my main, and this might be the reason I can't seem to make a PR... I'll learn at some point!

Owner

mseri commented on `a1a2abd` Feb 29, 2024

You need to make the changes to a branch on your repository (or this) and then you can make the pull request

Owner

mseri commented on `a1a2abd` Feb 29, 2024

I changed a setting in the repository: from now on we cannot push on main any longer, we can only send changes via pull request from other branches.

Please sign in to comment.