I wish to 'manually copy files to the USB stick — the flexible way'. I will be using either debian-9.4.0-i386-netinst.iso or a purchased DVD-1 of Debian 9.1.0 Section 4.3.3.2 says in part:
Mount the partition (mount /dev/sdX1 /mnt) and copy the following
installer image files to the stick:
vmlinuz or linux (kernel binary)
initrd.gz (initial ramdisk image)
You can choose between either the text-based or the graphical version
of the installer. The latter can be found in the gtk subdirectory. If
you want to rename the files, please note that syslinux can only process
DOS (8.3) file names.
In both sources I find a file named "vmlinuz". In neither source do I find a file named simply "linux". I do find "isolinux.bin" in both sources. What are the difference among those three. Which should I use? TIA