From 5cdb97c46573623549439cf4b0a266da18cb2d99 Mon Sep 17 00:00:00 2001 From: Antonio De Lucreziis Date: Fri, 29 Sep 2023 13:51:07 +0000 Subject: [PATCH] updated readme --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 9b74bc7..6e3c0d0 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ GitHub già offre 120h gratuite al mese di utilizzo di CodeSpace, inoltre [Unipi [![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?skip_quickstart=true&hide_repo_select=true&ref=main&repo=698191991&machine=standardLinux32gb&location=WestEurope) -**Attenzione!** Per non sprecare subito tutte le ore di utilizzo quando si ha finito di utilizzare il CodeSpace ricordarsi di spegnerlo dalla pagina , dalla lista di CodeSpaces se c'è scritto ancora "Active" premere sui tre puntini e fare "Stop Container". +:warning: Per non sprecare subito tutte le ore di utilizzo quando si ha finito di utilizzare il CodeSpace ricordarsi di spegnerlo dalla pagina , dalla lista di CodeSpaces se c'è scritto ancora "Active" premere sui tre puntini e fare "Stop Container". Per provare che tutto funzioni andare in `./Main.lean` e verificare che si apra il pannello laterale e che mettendo il mouse sopra `#eval` venga mostrata la stringa `Hello, World!`.