Update.
authorFrancois Fleuret <francois@fleuret.org>
Mon, 30 Aug 2021 12:56:43 +0000 (14:56 +0200)
committerFrancois Fleuret <francois@fleuret.org>
Mon, 30 Aug 2021 12:56:43 +0000 (14:56 +0200)
arxiv-rename-pdf.sh
bashrc
dhtml.sh

index 57b80c5..b165c5e 100755 (executable)
@@ -31,17 +31,17 @@ do
 
     if [[ $1 =~ ^http ]]
     then
-        wget "$1"
-        id="$(echo "$1" | sed -e 's|^.*/\([^\]*\)$|\1|')"
+        id="$(echo "$1" | sed -e 's|^.*/\([0-9.]*\)$|\1|')"
+        wget "https://arxiv.org/pdf/${id}"
         filename="${id}.pdf"
     else
         filename="$1"
         id="$(basename ${filename} .pdf)"
     fi
 
-    while [[ -f "$1.part" ]] # dealing with firefox's download
+    while [[ -f "${id}.pdf.part" ]] # dealing with firefox's download
     do
-        echo "Waiting for $1.part to vanish"
+        echo "Waiting for ${id}.pdf.part to vanish"
         sleep 1
     done
 
diff --git a/bashrc b/bashrc
index f312fc0..93b9e56 100644 (file)
--- a/bashrc
+++ b/bashrc
@@ -58,7 +58,7 @@ shopt -s autocd
 ######################################################################
 
 # added by Miniconda3 installer
-export PATH="/home/fleuret/conda/bin:$PATH"
+export PATH="${HOME}/conda/bin:$PATH"
 
 [ ${TERM} == "dumb" ] || [[ ! -t 0 ]] && return
 
@@ -819,7 +819,7 @@ function ripdvd () {
         return 1
     fi
 
-    echo "Attemptin to rip from ${DVD_DEVICE}."
+    echo "Attempting to rip from ${DVD_DEVICE}."
 
     mkdir -p ${HOME}/dvds
 
@@ -919,7 +919,7 @@ then
         git 2>/dev/null rev-parse --abbrev-ref HEAD | sed -e 's/^\(.*\)$/(\1) /'
     }
 
-    export PS_GIT="${VT_WHITE_BG}${VT_GREEN_FG}\$(parse_git_branch)${VT_RESET}"
+    export PS_GIT="${VT_GREEN_FG}\$(parse_git_branch)"
 fi
 
 ######################################################################
@@ -952,6 +952,8 @@ else
 
     [[ "${IDENT}" ]] && IDENT="${IDENT}:"
 
+    #    IDENT="${PS_GIT}${VT_BLACK_FG}${IDENT}"
+
     if [[ ${USER} == "root" ]]
     then
         # If we are root, show that in red
@@ -969,7 +971,7 @@ else
 
 fi
 
-PS1="${PS_GIT}${PSCUE}${PS1}"
+#PS1="${PSCUE}${PS1}"
 
 ######################################################################
 # This implements a local history. If we are in a directory containing
index 8b74fe2..cefb843 100755 (executable)
--- a/dhtml.sh
+++ b/dhtml.sh
@@ -69,6 +69,14 @@ do
         line=$(sed -e "s/@SIZE{\([^}]*\)}/${filesize_h}/" <<<"${line}")
     done
 
+    while [[ ${line} =~ @URLDATE ]]
+    do
+        filename=$(sed -e "s/^.*@URLDATE{\([^}]*\)}.*$/\1/" <<<"${line}")
+        timestamp=$(curl -Lv "${filename}" 2>&1 | \grep '^< Last-Modified:' | sed -e 's/^.*Last-Modified: *//')
+        timestamp=$(date -d "${timestamp}" +'%b %e, %Y')
+        line=$(sed -e "s/@URLDATE{\([^}]*\)}/${timestamp}/" <<<"${line}")
+    done
+
     while [[ ${line} =~ @FILEDATE ]]
     do
         filename=$(sed -e "s/^.*@FILEDATE{\([^}]*\)}.*$/\1/" <<<"${line}")