Rename dupfiles to dups
authorSiraaj Khandkar <siraaj@khandkar.net>
Wed, 14 Nov 2018 16:19:36 +0000 (11:19 -0500)
committerSiraaj Khandkar <siraaj@khandkar.net>
Wed, 14 Nov 2018 16:19:36 +0000 (11:19 -0500)
commit03db9aee3a879fdb6aef6b40d86b9aca3898a376
tree6e6ade770a6f7ce42697c464bd7bf2a4a7441540
parent0a1c6f40315940659978d3d576cc7c6415c27d81
Rename dupfiles to dups
.gitignore
Makefile
dups.ml [moved from dupfiles.ml with 100% similarity]
dups.mli [moved from dupfiles.mli with 100% similarity]
This page took 0.030149 seconds and 4 git commands to generate.