Really is !75; I made a false operation that removed it unduly

I used git push mine :intro_notebooks instead of git push origin intro_notebooks, which closed immediately !75 (closed)...

requested review from @vrouvrea

assigned to @sgilles

mentioned in merge request !75 (closed)

approved this merge request

merged

mentioned in commit 01067627