Lines Matching refs:vmlinux
181 --vmlinux=file vmlinux kernel image
182 --no-vmlinux no kernel image (vmlinux) available
328 VMLINUX=
421 echo "VMLINUX=$VMLINUX" >> $SETUP_FILE
461 if test -z "$VMLINUX"; then
462 echo "No vmlinux file specified. You must specify the correct vmlinux file, e.g." >&2
463 echo "opcontrol --vmlinux=/path/to/vmlinux" >&2
464 echo "If you do not have a vmlinux file, use " >&2
465 echo "opcontrol --no-vmlinux" >&2
470 if test -f "$VMLINUX"; then
474 if test "$VMLINUX" = "none"; then
478 echo "The specified vmlinux file \"$VMLINUX\" doesn't exist." >&2
508 FILE_IMAGE="$VMLINUX"
527 echo "Make sure you are using the non-compressed image file (e.g. vmlinux not vmlinuz)" >&2
837 --vmlinux)
839 VMLINUX=$val
842 --no-vmlinux)
843 VMLINUX=none
963 vecho "VMLINUX $VMLINUX"
1499 if test "$VMLINUX" = "none"; then
1500 OPD_ARGS="$OPD_ARGS --no-vmlinux"
1502 OPD_ARGS="$OPD_ARGS --vmlinux=$VMLINUX --kernel-range=$KERNEL_RANGE"
1585 echo "vmlinux file: $VMLINUX"
