From 2d57d6db17480b481429a13bea3d3e9560946949 Mon Sep 17 00:00:00 2001
From: Wenzel Jakob <wenzel.jakob@epfl.ch>
Date: Mon, 13 Jul 2020 17:58:33 +0200
Subject: [PATCH] rename Makefile -> Makefile.old

---
 Makefile => Makefile.old | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Makefile => Makefile.old (100%)

diff --git a/Makefile b/Makefile.old
similarity index 100%
rename from Makefile
rename to Makefile.old