From de9d34560af7869f776242de118111a6873197c0 Mon Sep 17 00:00:00 2001
From: Florent Pruvost <florent.pruvost@inria.fr>
Date: Thu, 9 Mar 2017 11:13:05 +0100
Subject: [PATCH] rename README-dev in order to make README.org the main entry
 point

---
 README-dev.org => READMEDEV.org | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename README-dev.org => READMEDEV.org (100%)

diff --git a/README-dev.org b/READMEDEV.org
similarity index 100%
rename from README-dev.org
rename to READMEDEV.org
-- 
GitLab