From 08c430c78ff8256d6ea4b1019dea40e34bbf2b3a Mon Sep 17 00:00:00 2001
From: Pietro <pietro.abate@inria.fr>
Date: Thu, 22 Feb 2018 11:07:26 +0100
Subject: [PATCH] Makefile: add 'fix-indent' target

---
 Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Makefile b/Makefile
index 05104e2da..76e608c39 100644
--- a/Makefile
+++ b/Makefile
@@ -53,6 +53,9 @@ test:
 test-indent:
 	@jbuilder build @runtest_indent ${DEV}
 
+fix-indent:
+	@src/lib_stdlib/test-ocp-indent.sh fix
+
 build-deps:
 	@./scripts/install_build_deps.sh