@affeldt-aist do you mind if I squash both our commits and put myself as co-authored-by, it makes no sense to keep the history... single commits are not compiling anymore anyway.
please, go ahead
are you still working on this PR ?
well, I did promise to do my homework by monday, true that I didn't have much time since yesterday :-(
May I ask what you are doing on it so that we do not collide?
(I think I did push something yesterday evening...)
ah!
we lost one commit!
oooh
sorry....
do you know the commit number ?
I still had my emacs buffer
I was about to tackle near_non(de|in)creasing_is_cvg
to be precise.
ok, thanks, I will do a fixup with it
Then I was planning to fix cesaro
and produce a few lemmas dual of already existing lemmas
and use this experience to feed the contributing guide
ok!
sorry, I pushed in a hurry and the CI didn't go through, let me fix this
I will merge math-comp/analysis#202 and rebase sequences on it
affeldt-aist said:
sorry, I pushed in a hurry and the CI didn't go through, let me fix this
I noticed already and it is almost fixed
ok, I let you do that (strangely it was compiling in emacs, something changed under my feet)
yes, I accidentally removed image_inj
(+ bounded changed a few other things under your feet)
I hope I did not loose more
could you give me the commit number ?
git rev-parse HEAD
d46f2364841b3cd0ceb85fee76d37a62a3f50a9d (yesterday's commit that disappeared)
a last rebase and I give it back
Last updated: Oct 13 2024 at 01:02 UTC