cli: formally deprecate --memory option
    
    That option had never a real effect, and we now don't even dropped the
    remaining parts of this idea in Frontend (PR#1480).
    
    So throw a warning if anyone by accident uses this option.  It also
    doesn't make sense to complicate the --help output by that option, so
    suppress it.