diff --git a/collects/embedded-gui/info.ss b/collects/embedded-gui/info.ss deleted file mode 100644 index c14a2ca4..00000000 --- a/collects/embedded-gui/info.ss +++ /dev/null @@ -1 +0,0 @@ -#lang setup/infotab diff --git a/collects/mrlib/private/aligned-pasteboard/info.ss b/collects/mrlib/private/aligned-pasteboard/info.ss new file mode 100644 index 00000000..865edce1 --- /dev/null +++ b/collects/mrlib/private/aligned-pasteboard/info.ss @@ -0,0 +1,3 @@ +#lang setup/infotab + +(define compile-omit-paths '("tests")) diff --git a/collects/web-server/tests/info.ss b/collects/web-server/tests/info.ss new file mode 100644 index 00000000..a073420a --- /dev/null +++ b/collects/web-server/tests/info.ss @@ -0,0 +1,3 @@ +#lang setup/infotab + +(define compile-omit-paths 'all)