{"action":"created","issue":{"url":"https://api.github.com/repos/metamath/set.mm/issues/116","repository_url":"https://api.github.com/repos/metamath/set.mm","labels_url":"https://api.github.com/repos/metamath/set.mm/issues/116/labels{/name}","comments_url":"https://api.github.com/repos/metamath/set.mm/issues/116/comments","events_url":"https://api.github.com/repos/metamath/set.mm/issues/116/events","html_url":"https://github.com/metamath/set.mm/pull/116","id":240027208,"number":116,"title":"Discouraged theorems replaced","user":{"login":"glacode","id":27626923,"avatar_url":"https://avatars1.githubusercontent.com/u/27626923?v=3","gravatar_id":"","url":"https://api.github.com/users/glacode","html_url":"https://github.com/glacode","followers_url":"https://api.github.com/users/glacode/followers","following_url":"https://api.github.com/users/glacode/following{/other_user}","gists_url":"https://api.github.com/users/glacode/gists{/gist_id}","starred_url":"https://api.github.com/users/glacode/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/glacode/subscriptions","organizations_url":"https://api.github.com/users/glacode/orgs","repos_url":"https://api.github.com/users/glacode/repos","events_url":"https://api.github.com/users/glacode/events{/privacy}","received_events_url":"https://api.github.com/users/glacode/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2017-07-02T18:43:36Z","updated_at":"2017-07-02T19:06:15Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/metamath/set.mm/pulls/116","html_url":"https://github.com/metamath/set.mm/pull/116","diff_url":"https://github.com/metamath/set.mm/pull/116.diff","patch_url":"https://github.com/metamath/set.mm/pull/116.patch"},"body":"The use of discouraged theorems has been fixed.\r\nA couple of theorems have been renamed (for naming consistency).\r\nTwo lemmas for wallispi2 have been moved to the proper position and wallispi lemmas have been renamed accordingly.\r\nSome weird spacing for statements has been fixed.\r\n(thanks to Mario for his stylistic comments)"},"comment":{"url":"https://api.github.com/repos/metamath/set.mm/issues/comments/312510654","html_url":"https://github.com/metamath/set.mm/pull/116#issuecomment-312510654","issue_url":"https://api.github.com/repos/metamath/set.mm/issues/116","id":312510654,"user":{"login":"digama0","id":868588,"avatar_url":"https://avatars0.githubusercontent.com/u/868588?v=3","gravatar_id":"","url":"https://api.github.com/users/digama0","html_url":"https://github.com/digama0","followers_url":"https://api.github.com/users/digama0/followers","following_url":"https://api.github.com/users/digama0/following{/other_user}","gists_url":"https://api.github.com/users/digama0/gists{/gist_id}","starred_url":"https://api.github.com/users/digama0/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/digama0/subscriptions","organizations_url":"https://api.github.com/users/digama0/orgs","repos_url":"https://api.github.com/users/digama0/repos","events_url":"https://api.github.com/users/digama0/events{/privacy}","received_events_url":"https://api.github.com/users/digama0/received_events","type":"User","site_admin":false},"created_at":"2017-07-02T19:06:15Z","updated_at":"2017-07-02T19:06:15Z","body":"It doesn't. This is fine for merging, and I think Norm will soon be\nfollowing up with cleanup of other mathboxes and updating the discouraged\nfile, which will fix the Travis errors.\n\nOn Sun, Jul 2, 2017 at 2:59 PM, glacode <notifications@github.com> wrote:\n\n> As I read the Travis trace, all Discouraged have the \"-\" sign in front,\n> but the exit code is still 1 (may be it doesn't discriminate between\n> removed and added references?)\n>\n> —\n> You are receiving this because you are subscribed to this thread.\n> Reply to this email directly, view it on GitHub\n> <https://github.com/metamath/set.mm/pull/116#issuecomment-312510289>, or mute\n> the thread\n> <https://github.com/notifications/unsubscribe-auth/AA1A7GV32F6EsP8dpWbyjp9g1nw2UX5Tks5sJ-h_gaJpZM4OLqKH>\n> .\n>\n"}}
{"actor":{"display_login":"digama0"}}