On Jan 31, 2017, at 01:45 , Emmanuel Charpentier wrote:
> Suggestion (I don't have Magma and can't try) : hit Ctrl-D (proabbly
> Command-d on a Mac), thus signalling an end of file to Magma. Or try the
> Magma command yyou type to end a terminal session.
FWIW, CMD-D on the Mac generally will d
Ctrl-D works, thanks!
On Tuesday, January 31, 2017 at 10:45:01 AM UTC+1, Emmanuel Charpentier
wrote:
>
> Suggestion (I don't have Magma and can't try) : hit Ctrl-D (proabbly
> Command-d on a Mac), thus signalling an end of file to Magma. Or try the
> Magma command yyou type to end a terminal se
Ctrl-D works, thanks!
On Tue, Jan 31, 2017 at 10:45 AM, Emmanuel Charpentier <
emanuel.charpent...@gmail.com> wrote:
> Suggestion (I don't have Magma and can't try) : hit Ctrl-D (proabbly
> Command-d on a Mac), thus signalling an end of file to Magma. Or try the
> Magma command yyou type to end a
Suggestion (I don't have Magma and can't try) : hit Ctrl-D (proabbly
Command-d on a Mac), thus signalling an end of file to Magma. Or try the
Magma command yyou type to end a terminal session.
HTH,
--
Emmanuel Charpentier
Le mardi 31 janvier 2017 10:37:24 UTC+1, Soli vishkautsan a écrit :
>
>
