1. 25 Oct, 2018 1 commit
  2. 03 Oct, 2018 1 commit
  3. 29 Sep, 2018 1 commit
  4. 26 Aug, 2018 1 commit
  5. 21 Jun, 2018 1 commit
  6. 10 Jun, 2018 2 commits
  7. 10 Jan, 2018 2 commits
    • Jonas Bernoulli's avatar
      Add PULL_REQUEST_TEMPLATE file · eb1677f1
      Jonas Bernoulli authored
      eb1677f1
    • Jonas Bernoulli's avatar
      Move Github-supported documentation files into sub-directory · 6ebc1772
      Jonas Bernoulli authored
      Unfortunately Github only finds these files if they are located at the
      top-level or in a sub-directory named either "docs" or ".github".  Our
      documentation directory is called "Documentation".
      
      We used to place these files at the top-level but since I am going to
      add more of the supported files this would become to noisy.  The best
      work around would be to create a symlink ".github -> Documentation,
      but Github doesn't support that.  The next best thing is to create a
      directory named ".github" that contains symlinks to files inside
      "Documentation".
      6ebc1772