{"push_id":3034907912,"size":11,"distinct_size":11,"ref":"refs/heads/custom-ext-html","head":"a03e166e6c26fb0c07676288a020c0a180713aa2","before":"1121d4a92baab1e8035d356d7a5051675c87e7d1","commits":[{"sha":"a912c829bfa5b6dce90a8dc9ebeafadf5ee34892","author":{"name":"G. Allais","email":"60a54f938b6c3401112164cd81a3e51650ab7fb0@ens-lyon.org"},"message":" [ fix #3315 ] primEraseEquality together with without-K is unsafe","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/a912c829bfa5b6dce90a8dc9ebeafadf5ee34892"},{"sha":"6cfe57d226d432ce62ab9e5d2aa9f9a5cac77d3a","author":{"name":"Tesla Ice Zhang","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"Fix broken link","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/6cfe57d226d432ce62ab9e5d2aa9f9a5cac77d3a"},{"sha":"c5cbc7e8017a3b9e28e271dfb7f50dbabb14f3d9","author":{"name":"Nils Anders Danielsson","email":"43f2a2d2c86e22bc80f5acc690d97a5dcf4c4b2f@cse.gu.se"},"message":"[ #3315 ] Renamed EraseEquality to Equality.Erase.","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/c5cbc7e8017a3b9e28e271dfb7f50dbabb14f3d9"},{"sha":"ffecec4a177270c0144c94b7b43cd5f51e9c3580","author":{"name":"Nils Anders Danielsson","email":"43f2a2d2c86e22bc80f5acc690d97a5dcf4c4b2f@cse.gu.se"},"message":"[ #3318 ] Added Agda.Builtin.Equality.Rewrite.","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/ffecec4a177270c0144c94b7b43cd5f51e9c3580"},{"sha":"a9bad1b86448c78f3e3fcadbb1c958b1894a8387","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3366 ] Added initial support, will document later\n\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/a9bad1b86448c78f3e3fcadbb1c958b1894a8387"},{"sha":"c285779e5ee41ce2d3864e4dddd28a25abc51bd4","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3366 ] Refactor file type detection, add `iFileType` field for `Interface`\n\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/c285779e5ee41ce2d3864e4dddd28a25abc51bd4"},{"sha":"b0372dcc4a7cd4f18b36b6cc7e8cdb5d65ce0d26","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3366 ] Fix typo\n\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/b0372dcc4a7cd4f18b36b6cc7e8cdb5d65ce0d26"},{"sha":"6c5bcd9507635861f9726cf2bdce02a69810662b","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3366 ] Address comments","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/6c5bcd9507635861f9726cf2bdce02a69810662b"},{"sha":"cf866969ec3ddbd820acad8417e989b3831faa3c","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ doc ] Documentation and changelog for #3366","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/cf866969ec3ddbd820acad8417e989b3831faa3c"},{"sha":"1ef929fa418029e0343f5700f864c2a70e190fae","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3366 ] Address comments\n\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/1ef929fa418029e0343f5700f864c2a70e190fae"},{"sha":"a03e166e6c26fb0c07676288a020c0a180713aa2","author":{"name":"Tesla Ice Zhang","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ tests ] Added some tests about `--html-highlight` flags, with `auto` and `code` and `all` (#1)","distinct":true,"url":"https://api.github.com/repos/Agda-zh/agda/commits/a03e166e6c26fb0c07676288a020c0a180713aa2"}]}
{"actor":{"display_login":"ice1000"}}