annotate .hgignore @ 0:99728ee0d697

day 1...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 20 Feb 2020 19:52:51 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 syntax:glob
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 # Created by https://www.gitignore.io/api/agda
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 # Edit at https://www.gitignore.io/?templates=agda
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 ### Agda ###
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 *.agdai
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 MAlonzo/**
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
99728ee0d697 day 1...
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 # End of https://www.gitignore.io/api/agda