diff options
author | sternenseemann <git@lukasepple.de> | 2020-04-30 20:03:46 +0200 |
---|---|---|
committer | sternenseemann <git@lukasepple.de> | 2020-04-30 20:03:46 +0200 |
commit | a6b682958df704e0bf50c9135ab779c2ee8e9cb8 (patch) | |
tree | 564cd3f643180af21ac07407430e9797da1756b7 | |
parent | 6c9228ccc8de0d758211ebbeeca1a77fdcc2d811 (diff) |
Remove _tags file
-rw-r--r-- | _tags | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/_tags b/_tags deleted file mode 100644 index 4123a24..0000000 --- a/_tags +++ /dev/null @@ -1,4 +0,0 @@ -true : bin_annot, safe_string, package(bytes ptime angstrom astring) -<src> : include - -<src/logbook*> : package(lwt lwt.unix jingoo cow) |