diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/boot-source-footer.e | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/language/boot-source-footer.e b/language/boot-source-footer.e new file mode 100644 index 0000000..97a8c5b --- /dev/null +++ b/language/boot-source-footer.e @@ -0,0 +1,6 @@ +~ This file should be included in executables that use boot-source, as the +~ last thing in the boot-source. It has the responsibility of switching from +~ processing boot-source into the regular interaction mode. + +relink-main-input-buffer-to-stdin + |