From 03db9aee3a879fdb6aef6b40d86b9aca3898a376 Mon Sep 17 00:00:00 2001 From: Siraaj Khandkar Date: Wed, 14 Nov 2018 11:19:36 -0500 Subject: [PATCH] Rename dupfiles to dups --- .gitignore | 2 +- Makefile | 2 +- dupfiles.ml => dups.ml | 0 dupfiles.mli => dups.mli | 0 4 files changed, 2 insertions(+), 2 deletions(-) rename dupfiles.ml => dups.ml (100%) rename dupfiles.mli => dups.mli (100%) diff --git a/.gitignore b/.gitignore index 7d19a9d..df36a51 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,5 @@ _build/ -dupfiles +dups *.native *.native *.swp diff --git a/Makefile b/Makefile index 3e9627e..13520a8 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -EXE_NAME := dupfiles +EXE_NAME := dups EXE_TYPE := native .PHONY: all build clean diff --git a/dupfiles.ml b/dups.ml similarity index 100% rename from dupfiles.ml rename to dups.ml diff --git a/dupfiles.mli b/dups.mli similarity index 100% rename from dupfiles.mli rename to dups.mli -- 2.20.1