{"action":"created","issue":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/242","labels_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/242/labels{/name}","comments_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/242/comments","events_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/242/events","html_url":"https://github.com/GaloisInc/cryptol/issues/242","id":88868122,"number":242,"title":"Comments with multiple stars fail to parse","user":{"login":"atomb","id":24929,"avatar_url":"https://avatars.githubusercontent.com/u/24929?v=3","gravatar_id":"","url":"https://api.github.com/users/atomb","html_url":"https://github.com/atomb","followers_url":"https://api.github.com/users/atomb/followers","following_url":"https://api.github.com/users/atomb/following{/other_user}","gists_url":"https://api.github.com/users/atomb/gists{/gist_id}","starred_url":"https://api.github.com/users/atomb/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/atomb/subscriptions","organizations_url":"https://api.github.com/users/atomb/orgs","repos_url":"https://api.github.com/users/atomb/repos","events_url":"https://api.github.com/users/atomb/events{/privacy}","received_events_url":"https://api.github.com/users/atomb/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-06-16T23:43:37Z","updated_at":"2015-06-20T19:24:02Z","closed_at":null,"body":"The following Cryptol file:\r\n\r\n```\r\n/**** Blah ****/\r\n```\r\nfails to load with a parse error. Changing it to this:\r\n```\r\n/* *** Blah *** */\r\n```\r\nallows it to work."},"comment":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/comments/113807876","html_url":"https://github.com/GaloisInc/cryptol/issues/242#issuecomment-113807876","issue_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/242","id":113807876,"user":{"login":"weaversa","id":7407930,"avatar_url":"https://avatars.githubusercontent.com/u/7407930?v=3","gravatar_id":"","url":"https://api.github.com/users/weaversa","html_url":"https://github.com/weaversa","followers_url":"https://api.github.com/users/weaversa/followers","following_url":"https://api.github.com/users/weaversa/following{/other_user}","gists_url":"https://api.github.com/users/weaversa/gists{/gist_id}","starred_url":"https://api.github.com/users/weaversa/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/weaversa/subscriptions","organizations_url":"https://api.github.com/users/weaversa/orgs","repos_url":"https://api.github.com/users/weaversa/repos","events_url":"https://api.github.com/users/weaversa/events{/privacy}","received_events_url":"https://api.github.com/users/weaversa/received_events","type":"User","site_admin":false},"created_at":"2015-06-20T19:24:02Z","updated_at":"2015-06-20T19:24:02Z","body":"I usually write things like:\r\n```\r\n/**************************************************\r\n  Here is documentation about this function...\r\n  blah blah blah\r\n***************************************************/\r\n```\r\nI gather this isn't possible anymore.\r\n\r\nPerhaps, instead of a parse error, Cryptol could (correctly) assume that we are not entering a docstring, but rather just putting text in a comment. Really, any sequence of characters should be valid inside a block comment (except */ which ends the comment). So, if it's not a correctly formatted docstring, why not just assume it's not a docstring, and move on, rather than producing an error?"}}