diff --git a/proposal/myrmidon/docs.xml b/proposal/myrmidon/docs.xml index 4fdd6cca7..9f20c502e 100644 --- a/proposal/myrmidon/docs.xml +++ b/proposal/myrmidon/docs.xml @@ -4,7 +4,7 @@ Give user a chance to override without editing this file (and without typing -D each time he compiles it) --> - +