GitHub's milestone tool: A mixed‐methods analysis on its use. Issue 4 (20th November 2019)