#] 
#] *********************
#] "$d_SysMaint"'Linux/tar notes.txt'
# www.BillHowell.ca  29Jan2024 initial 
# view in text editor, using constant-width font (eg courier), tabWidth = 3

#48************************************************48




#24************************24
# Table of Contents, generate with :
# $ grep  "^#]"  "$d_SysMaint"'Linux/tar notes.txt' |  sed "s/^#\]/  /" 
#


#24************************24
# Setup, ToDos,   


#08********08
#] ??Jan2024 


#08********08
#] ??Jan2024 


#08********08
#] ??Jan2024 


#08********08
#] ??Jan2024 


#08********08
#] ??Jan2024 


#08********08
#] 29Jan2024 man tar, example of Isabelle math prover

https://isabelle.in.tum.de/installation.html
/home/bill/PROJECTS/SW install & maintain/Isabelle
nyet: mv to /home/bill/web/CompLangs/math proof Isabelle

$ cd "$d_web"'CompLangs/'
$ tar -xzf "$d_PROJECTS"'SW install & maintain/Isabelle/Isabelle2023_linux.tar.gz'
>> awesome works well

       -f, --file=ARCHIVE
              Use  archive  file or device ARCHIVE.  If this option is not given, tar will first examine the envi‐
              ronment variable `TAPE'.  If it is set, its value will be used as the archive name.  Otherwise,  tar
              will assume the compiled-in default.  The default value can be inspected either using the --show-de‐
              faults option, or at the end of the tar --help output.

              An archive name that has a colon in it specifies a file or device on a remote machine.  The part be‐
              fore  the colon is taken as the machine name or IP address, and the part after it as the file or de‐
              vice pathname, e.g.:

              --file=remotehost:/dev/sr0

              An optional username can be prefixed to the hostname, placing a @ sign between them.

              By default, the remote host is accessed via the rsh(1) command.  Nowadays it is common to use ssh(1)
              instead.  You can do so by giving the following command line option:

              --rsh-command=/usr/bin/ssh

              The  remote  machine should have the rmt(8) command installed.  If its pathname does not match tar's
              default, you can inform tar about the correct pathname using the --rmt-command option.

       -x, --extract, --get
              Extract  files  from an archive.  Arguments are optional.  When given, they specify names of the ar‐
              chive members to be extracted.

       -z, --gzip, --gunzip, --ungzip
              Filter the archive through gzip(1).



# enddoc