{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6741","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6741/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6741/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6741/events","html_url":"https://github.com/coq/coq/pull/6741","id":296417835,"number":6741,"title":"coq_makefile: Support \"\" as the prefix in _CoqProject","user":{"login":"nomeata","id":148037,"avatar_url":"https://avatars2.githubusercontent.com/u/148037?v=4","gravatar_id":"","url":"https://api.github.com/users/nomeata","html_url":"https://github.com/nomeata","followers_url":"https://api.github.com/users/nomeata/followers","following_url":"https://api.github.com/users/nomeata/following{/other_user}","gists_url":"https://api.github.com/users/nomeata/gists{/gist_id}","starred_url":"https://api.github.com/users/nomeata/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nomeata/subscriptions","organizations_url":"https://api.github.com/users/nomeata/orgs","repos_url":"https://api.github.com/users/nomeata/repos","events_url":"https://api.github.com/users/nomeata/events{/privacy}","received_events_url":"https://api.github.com/users/nomeata/received_events","type":"User","site_admin":false},"labels":[{"id":485985650,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20fix","name":"kind: fix","color":"d93f0b","default":false},{"id":723364282,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20regression","name":"kind: regression","color":"e00403","default":false},{"id":723364180,"url":"https://api.github.com/repos/coq/coq/labels/part:%20tools","name":"part: tools","color":"dddddd","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/11","html_url":"https://github.com/coq/coq/milestone/11","labels_url":"https://api.github.com/repos/coq/coq/milestones/11/labels","id":2974954,"number":11,"title":"8.7.2","description":"","creator":{"login":"Zimmi48","id":1108325,"avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","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},"open_issues":16,"closed_issues":57,"state":"open","created_at":"2017-12-12T16:52:07Z","updated_at":"2018-02-12T16:40:54Z","due_on":"2018-02-15T08:00:00Z","closed_at":null},"comments":3,"created_at":"2018-02-12T15:35:26Z","updated_at":"2018-02-12T18:54:13Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/6741","html_url":"https://github.com/coq/coq/pull/6741","diff_url":"https://github.com/coq/coq/pull/6741.diff","patch_url":"https://github.com/coq/coq/pull/6741.patch"},"body":"This fixes #6350 (and even comes with a test case).\r\n\r\nRefering to other directories as `-R … \"\"` is maybe not best practice,\r\nbut some people out there do it, so as long as it does not cause too\r\nmuch trouble, we can continue to support it."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/365024572","html_url":"https://github.com/coq/coq/pull/6741#issuecomment-365024572","issue_url":"https://api.github.com/repos/coq/coq/issues/6741","id":365024572,"user":{"login":"SkySkimmer","id":2461932,"avatar_url":"https://avatars1.githubusercontent.com/u/2461932?v=4","gravatar_id":"","url":"https://api.github.com/users/SkySkimmer","html_url":"https://github.com/SkySkimmer","followers_url":"https://api.github.com/users/SkySkimmer/followers","following_url":"https://api.github.com/users/SkySkimmer/following{/other_user}","gists_url":"https://api.github.com/users/SkySkimmer/gists{/gist_id}","starred_url":"https://api.github.com/users/SkySkimmer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SkySkimmer/subscriptions","organizations_url":"https://api.github.com/users/SkySkimmer/orgs","repos_url":"https://api.github.com/users/SkySkimmer/repos","events_url":"https://api.github.com/users/SkySkimmer/events{/privacy}","received_events_url":"https://api.github.com/users/SkySkimmer/received_events","type":"User","site_admin":false},"created_at":"2018-02-12T18:54:13Z","updated_at":"2018-02-12T18:54:13Z","author_association":"CONTRIBUTOR","body":"Try CString.is_empty, it's in Coq's extended library.\n\nGaëtan Gilbert\n\nOn 12/02/2018 19:53, Joachim Breitner wrote:\n> *@nomeata* commented on this pull request.\n> \n> ------------------------------------------------------------------------\n> \n> In tools/coq_makefile.ml \n> <https://github.com/coq/coq/pull/6741#discussion_r167651494>:\n> \n>> @@ -124,7 +124,7 @@ let read_whole_file s =\n>       close_in ic;\n>       Buffer.contents b\n>   \n> -let quote s = if String.contains s ' ' || String.equal s \"\" then \"'\" ^ s ^ \"'\" else s\n> +let quote s = if String.contains s ' ' || s = \"\" then \"'\" ^ s ^ \"'\" else s\n>   \n> \n> Hm, doesn't work here:\n> \n> |File \"tools/coq_makefile.ml\", line 127, characters 42-57: Error: Unbound \n> value String.is_empty |\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/coq/coq/pull/6741#discussion_r167651494>, or mute \n> the thread \n> <https://github.com/notifications/unsubscribe-auth/ACWQ7BblmidQqkoRoYUarHLPMI_LR212ks5tUIijgaJpZM4SCWzU>.\n> \n"}}
{"actor":{"display_login":"SkySkimmer"}}