VSCode の制限モード

なんか、そんなものが追加されたらしく、

　　学生に Agda Extension 使ってもらったら動かない

この外し方が、また、良くわからない。まぁ、

　　VSCode の高機能とブラウザ依存の脆弱性

を考えると、そうかなとも思うんですが、

　　自分で入れた Agda Exteion を使うのに、ググって探す

ってのはどうなの? この、そびえたつくそを授業のページに書くのは残念かな。