{"push_id":3058366915,"size":21,"distinct_size":21,"ref":"refs/heads/master","head":"3161248c2dcde48c19246b125a7a2ad0785d9d7a","before":"979507b9194a355599ad6abfa4f6f1fef5b44d0b","commits":[{"sha":"2faff03275b84fc7416e5076f071e7505b366d6a","author":{"name":"Andrés Sicard-Ramírez","email":"1294692e88bc3cf578b0cf93126b82e453a3a24f@eafit.edu.co"},"message":"[ releases notes ] Added contributor entry.\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/2faff03275b84fc7416e5076f071e7505b366d6a"},{"sha":"afa864349f8afd5b43d839ecf1ce63dba734c536","author":{"name":"Andrés Sicard-Ramírez","email":"1294692e88bc3cf578b0cf93126b82e453a3a24f@eafit.edu.co"},"message":"[ user manual ] Added link the the LICENSE file.\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/afa864349f8afd5b43d839ecf1ce63dba734c536"},{"sha":"8c8103f06e90d427c1737f2a2c31435174d5cad1","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ doc ] Update contributor lists\n\n[ci skip]\n\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/8c8103f06e90d427c1737f2a2c31435174d5cad1"},{"sha":"2d980891f570cf4a50b8e8843eb9c5269b4d888e","author":{"name":"Tesla Ice Zhang","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ close #3373 ] Implement the proposed feature (#3384)\n\n* [ close #3373 ] Implementation, basic test case\r\n\r\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>\r\n\r\n* [ #3373 ] Add auto test, generate `.rst` files when `--html-highlight=auto`\r\n\r\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>\r\n\r\n* [ #3373 ] Move functions, document the change\r\n\r\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/2d980891f570cf4a50b8e8843eb9c5269b4d888e"},{"sha":"90abfcd365004fc65c5c1d0b835ff5bbad2bee7c","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ doc ] Fix typos\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/90abfcd365004fc65c5c1d0b835ff5bbad2bee7c"},{"sha":"2f6987ef77ac3d853c81be4507e8fe2bdc5f3162","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ doc ] Capitalization and alphabetical related issues\n\n[ci skip]\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/2f6987ef77ac3d853c81be4507e8fe2bdc5f3162"},{"sha":"dc3a6ac62612b8b075c54a17d572e85ebf6dfe92","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3379 ] Add link to agda wiki on `overview`\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/dc3a6ac62612b8b075c54a17d572e85ebf6dfe92"},{"sha":"d2ef69573b2448baf84e771050d24a9f822428cf","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ fix #3379 ] Add a tutorial list\n\nSigned-off-by: ice1000 <ice1000kotlin@foxmail.com>","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/d2ef69573b2448baf84e771050d24a9f822428cf"},{"sha":"13b1aa80d78375a915f08e237fc0f104c2afdfb8","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3379 ] More, fix format\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/13b1aa80d78375a915f08e237fc0f104c2afdfb8"},{"sha":"8a72309d82c6f02b9545d07433e2ef263582ee7e","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3379 ] Add some course links\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/8a72309d82c6f02b9545d07433e2ef263582ee7e"},{"sha":"bf006990deb7d066a1d34c5652fe9e8161119051","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3379 ] Fix reStructuredText format\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/bf006990deb7d066a1d34c5652fe9e8161119051"},{"sha":"ce5817270e18149bc773d2c378202617581e8014","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ #3379 ] Indentation fix (maybe next time I'll open a pull request for documentation changes?)\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/ce5817270e18149bc773d2c378202617581e8014"},{"sha":"018ad1b332e8321ffa3bc6263e2c1aa64a08dd95","author":{"name":"Andrés Sicard-Ramírez","email":"1294692e88bc3cf578b0cf93126b82e453a3a24f@eafit.edu.co"},"message":"[ doc ] Fixed URL.\n\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/018ad1b332e8321ffa3bc6263e2c1aa64a08dd95"},{"sha":"4d6d45000e71b1becd18e661fefd004c5d5c3e27","author":{"name":"ice1000","email":"6ee4fa7be887322cf4061fa0d2353d72aa471fa7@foxmail.com"},"message":"[ fix #3379 ] Use anonymous links\n[ci skip]","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/4d6d45000e71b1becd18e661fefd004c5d5c3e27"},{"sha":"a9d4392fa13efb63e886a3bbf8df59fbdde74d15","author":{"name":"Guillaume Allais","email":"60a54f938b6c3401112164cd81a3e51650ab7fb0@ens-lyon.org"},"message":"[ fix ] whitespace violation","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/a9d4392fa13efb63e886a3bbf8df59fbdde74d15"},{"sha":"055241079e33ea43fa8f97a0b1db149e8ec70ec5","author":{"name":"Jesper Cockx","email":"e3c7ff9230a78519a00220830d65110ea0beeed2@sikanda.be"},"message":"[ fix #1602 ] Stop abusing shape-irrelevance as runtime-erasure","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/055241079e33ea43fa8f97a0b1db149e8ec70ec5"},{"sha":"b5251f9511ceb26f1e96d09faa1e705d962f0c07","author":{"name":"Jesper Cockx","email":"e3c7ff9230a78519a00220830d65110ea0beeed2@sikanda.be"},"message":"[ #1602 ] Forgot to add one changed test file","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/b5251f9511ceb26f1e96d09faa1e705d962f0c07"},{"sha":"3ba41e022d5636e495846fd6b96ec02853f20d2f","author":{"name":"Jesper Cockx","email":"e3c7ff9230a78519a00220830d65110ea0beeed2@sikanda.be"},"message":"[ fix #3387 ] Document how to use private instances","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/3ba41e022d5636e495846fd6b96ec02853f20d2f"},{"sha":"8f747983568319f8cc4d9aaaf7a1f0a71d68eceb","author":{"name":"Andreas Abel","email":"dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de"},"message":"[ fixed #3394 ] forgotten initialization of terSizeDepth in termType","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/8f747983568319f8cc4d9aaaf7a1f0a71d68eceb"},{"sha":"bbb55ed717b7958051db95cb2f94e4f4c3c64af8","author":{"name":"Andreas Abel","email":"dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de"},"message":"[ #3393 ] Unsuccessful attempt to fix\n\nWhen we want to create an interface for the main file with\n--allow-unsolved-metas , we need to do it in a way that\npreserves the state such that after serialization the user\ncan continue working on open goals (which otherwise during\nserialization would have been replaced by postulates).","distinct":true,"url":"https://api.github.com/repos/mortberg/agda/commits/bbb55ed717b7958051db95cb2f94e4f4c3c64af8"}]}
{"actor":{"display_login":"mortberg"}}