diff -r e0323036bcf2 -r 1a604efd267d etc/settings
--- a/etc/settings	Sat Jun 14 17:26:09 2008 +0200
+++ b/etc/settings	Sat Jun 14 17:26:10 2008 +0200
@@ -67,13 +67,6 @@
 #ML_OPTIONS=""
 #ML_PLATFORM=""
 
-# Poplog/PML version 15.6/2.1 (experimental!)
-#ML_SYSTEM=poplogml
-#ML_HOME="/usr/local/poplog/current-poplog/bin"
-#ML_OPTIONS="-noinit"
-#ML_SUFFIX=".psv"
-#ML_PLATFORM=""
-
 
 ###
 ### Interactive sessions (cf. isatool tty)