diff --git a/examples/dgamelaunch.conf b/examples/dgamelaunch.conf
index 364225e..a5f92c0 100644
--- a/examples/dgamelaunch.conf
+++ b/examples/dgamelaunch.conf
@@ -57,6 +57,7 @@ bannervars = [ "$MOTDTIME" = "2011.10.08",
 # - bannervars from above
 # - $VERSION replaced with "dgamelaunch v" + dgl version number.
 # - $USERNAME replaced with logged-in user's name, or with "[Anonymous]"
+# - $INCLUDE(filename) the named file will be inserted here.
 banner = "/dgl-banner"
 
 # The following two options are fairly insecure. They will force us to