diff --git a/samples/PHP/root.php b/samples/PHP/root.php
new file mode 100644
index 00000000..8f8be563
--- /dev/null
+++ b/samples/PHP/root.php
@@ -0,0 +1,6 @@
+<?php
+  ////////////////////////////////////
+  // I am not Isabelle ROOT         //
+  ////////////////////////////////////
+
+?>