From a7c15c3049e21faa5987c8d2510508d6d9818a5d Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 5 Feb 2018 16:05:30 +1100 Subject: [PATCH] Change name --- minizinc.iro | 22 ++++------------------ 1 file changed, 4 insertions(+), 18 deletions(-) diff --git a/minizinc.iro b/minizinc.iro index 90a544b..2ec4ee5 100644 --- a/minizinc.iro +++ b/minizinc.iro @@ -1,27 +1,13 @@ ################################################################# -## Iro +## MiniZinc ################################################################ ## -## * Press Ctrl + '+'/'-' To Zoom in -## * Press Ctrl + S to save and recalculate... -## * Documents are saved to web storage. -## * Only one save slot supported. -## * Matches cannot span lines. -## * Unicode chars must be defined in \u0000 to \uffff format. -## * All matches must be contained by a single group ( ... ) -## * Look behinds not permitted, (?<= or (?