{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/618","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/618/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/618/comments","events_url":"https://api.github.com/repos/coq/coq/issues/618/events","html_url":"https://github.com/coq/coq/pull/618","id":226850297,"number":618,"title":"Possibility of different warning defaults in compilation and interactive mode","user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars2.githubusercontent.com/u/460771?v=3","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2017-05-07T11:10:33Z","updated_at":"2017-05-09T18:00:19Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/618","html_url":"https://github.com/coq/coq/pull/618","diff_url":"https://github.com/coq/coq/pull/618.diff","patch_url":"https://github.com/coq/coq/pull/618.patch"},"body":"This is a modest proposal for clarifying the status of the `invalid-identifier` and for giving the possibility of different default warnings in compilation and interactive mode as motivated in the discussion about generated name warning [#268](https://github.com/coq/coq/pull/268#issuecomment-299456681)."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/300250953","html_url":"https://github.com/coq/coq/pull/618#issuecomment-300250953","issue_url":"https://api.github.com/repos/coq/coq/issues/618","id":300250953,"user":{"login":"Zimmi48","id":1108325,"avatar_url":"https://avatars1.githubusercontent.com/u/1108325?v=3","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"created_at":"2017-05-09T18:00:18Z","updated_at":"2017-05-09T18:00:18Z","body":"@maximedenes The only use case so far is the warning on generated names. We can't merge PR #268 currently without breaking havoc in Travis because the log files become too long (because too many warnings are generated). In interactive mode, you are typically seeing only one warning at a time (and then you can even take the opportunity to fix it).\r\nI came up with this idea because, if the default is always off, this warning won't prove fruitful (most users use the default settings, and won't see it ever)."}}
{"actor":{"display_login":"Zimmi48"}}