hg and git

やっぱり、削除書くかと思って、RedBlackTree のrepository を見直してたら

　hg 側の uncommit change がある
　しかも、.git/hoge...

log を見ると、2023なB4がやらかしたらしい。まぁ、そうか

　hg rm -rf .git

なんだが、git 側が消えるのはよろしくないので、rsync で backup してから

なんだが、やっぱり触られてしまうらしい

開発用は hg で、github への commit は git という使いわけですけどね

肝心の削除の方は手つかず。めんどくさいんだよ

https://github.com/shinji-kono/gearsAgda/blob/main/BTree.agda
-