Caching make dev Web server #6

Open
opened 2025-07-07 15:24:35 +02:00 by Utopiah · 0 comments
Collaborator

Relying on redbean.dev is an option over e.g. NodeJS or Python (usually available, even though not always) 1-liners e.g. https://gist.github.com/stephenbradshaw/a2b72b5b58c93ca74b54f7747f18a481 that might be easier to maintain cross-platform.

At the moment though it downloads it every time, which can be slow on devices without a good connection.

Consequently one could consider

  if [ ! -f //tmp/server.com ]; then
    echo "Server not found!"
    wget "$REDBEAN_VERSION" -O /tmp/server.com 
    chmod +x /tmp/server.com 
  fi

to check if the server is present and only download if not.

This overall makes restarting ./make dev much faster.

Relying on `redbean.dev` is an option over e.g. NodeJS or Python (usually available, even though not always) 1-liners e.g. https://gist.github.com/stephenbradshaw/a2b72b5b58c93ca74b54f7747f18a481 that might be easier to maintain cross-platform. At the moment though it downloads it every time, which can be slow on devices without a good connection. Consequently one could consider ``` if [ ! -f //tmp/server.com ]; then echo "Server not found!" wget "$REDBEAN_VERSION" -O /tmp/server.com chmod +x /tmp/server.com fi ``` to check if the server is present and only download if not. This overall makes restarting `./make dev` much faster.
Sign in to join this conversation.
No labels
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: xrsh/xrsh#6
No description provided.