Closed JKRhb closed 1 year ago
Unfortunately, I don't think we want to delete the IMAGES directory under note3 since it was a record of a previous publication. Can you do a new PR with just the changes to index.html? I don't see why github is bothering you if you don't modify those files...
Unfortunately, I don't think we want to delete the IMAGES directory under note3 since it was a record of a previous publication. Can you do a new PR with just the changes to index.html? I don't see why github is bothering you if you don't modify those files...
Thank you for the feedback! I assume it was a problem specific to the machine I used at the time, on a different system I was now able to push the changes without a change to the IMAGES directory (i.e., I was able to drop the commit deleting it).
Some improvements needed:
Smaller improvements e.g. to wording should be done using github suggestions
This contains an initial attempt at expanding the introduction section. There is still some work to be done, but I think it could already be reviewed. I will try to finish it until the meeting on Monday.
I also had to remove the IMAGES file in this PR in order to be able to push the commit. Let me know if the file is too important to be deleted, then I will try to find a different solution for submitting this PR.Preview | Diff