Collection of themes/skins for the Fossil SCM

⌈⌋ ⎇ branch:  Fossil Skins Extra


Check-in [62d3073b30]

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fix change detection
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1: 62d3073b30bf4e9645199b51e7f645f02ba1477a
User & Date: mario 2021-09-06 03:02:29
Context
2021-09-19
09:31
crude survey tool (storage backend only) check-in: 43bb630b42 user: mario tags: trunk
2021-09-06
03:02
Fix change detection check-in: 62d3073b30 user: mario tags: trunk
2021-09-05
06:50
shorthand $EDITOR for wiki pages check-in: 7dc5402ce6 user: mario tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Name change from tools/fossileditwiki to tools/fossilwikiedit. 

1
2
3

4







5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22





23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

#!/bin/sh
# title: edit wiki page
# description: checkout/checkin doc page from fossil repo, edit via $EDITOR









# pagename
if [ -z "$1" ]
then
  echo Syntax: $0 PageName
  exit
fi
PAGE="$1"
EXISTS=0
SAVE=0

# test
EXISTS=$(fossil wiki ls | egrep "^$PAGE$")
if [ ! $EXISTS ]
then
  PAGE=$(fossil wiki ls | egrep -i "^$PAGE$")
  if [ -n "$PAGE" ]
  then
    echo "Found similar page name: '$PAGE'"





  fi
fi

# export
FILE=".f-w.$PAGE"
fossil wiki export "$PAGE" "$FILE"

# edit
MD5=$(md5sum "$FILE")
$EDITOR $FILE
MD5NEW=$(md5sum "$FILE")
if [ "$MD5NEW" != "$MD5" ]
then
  SAVE=1
fi

# save?
if [ $SAVE ]
then
  if [ $EXISTS ]
  then
    fossil wiki commit "$PAGE" "$FILE"
  else
    fossil wiki create "$PAGE" "$FILE" --mimetype text/x-markdown
  fi




>
|
>
>
>
>
>
>
>

|




<
<
<





|



>
>
>
>
>




|






<
<
<
<


|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18



19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43




44
45
46
47
48
49
50
51
52
53

#!/bin/sh
# title: edit wiki page
# description: checkout/checkin doc page from fossil repo, edit via $EDITOR
# version: 0.2
#
# Edits or creates new wiki page using local editor.
#
PAGE="$1"
FILE=""
ADDFN=""
EXISTS=0

# pagename
if [ -z "$PAGE" ]
then
  echo Syntax: $0 PageName
  exit
fi




# test
EXISTS=$(fossil wiki ls | egrep "^$PAGE$")
if [ ! $EXISTS ]
then
  PAGE=$(fossil wiki ls|egrep -m1 -i "^$PAGE$" || fossil wiki ls|grep -m1 -i "$PAGE")
  if [ -n "$PAGE" ]
  then
    echo "Found similar page name: '$PAGE'"
    EXISTS=1
  else
    PAGE=$1
    echo "New page: '$PAGE'"
    ADDFN=".new"
  fi
fi

# export
FILE="/tmp/fossileditwiki$ADDFN.$PAGE"
fossil wiki export "$PAGE" "$FILE"

# edit
MD5=$(md5sum "$FILE")
$EDITOR $FILE
MD5NEW=$(md5sum "$FILE")





# save?
if [ "$MD5NEW" != "$MD5" ]
then
  if [ $EXISTS ]
  then
    fossil wiki commit "$PAGE" "$FILE"
  else
    fossil wiki create "$PAGE" "$FILE" --mimetype text/x-markdown
  fi
︙︙