From 76f3df13206cc66999bb7b7b07f54a7310c58694 Mon Sep 17 00:00:00 2001 From: Zeno Rogue Date: Wed, 6 Mar 2019 16:32:38 +0100 Subject: [PATCH] CLI option -geo recognizes menu_displayed_names --- geom-exp.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/geom-exp.cpp b/geom-exp.cpp index 2aa3fa7a..4ba117e6 100644 --- a/geom-exp.cpp +++ b/geom-exp.cpp @@ -763,6 +763,18 @@ void runGeometryExperiments() { } #if CAP_COMMANDLINE + +eGeometry readGeo(const string& ss) { + bool numeric = true; + for(char c: ss) if(c < '0' || c > '9') numeric = false; + if(numeric) return eGeometry(atoi(ss.c_str())); + for(int i=0; i